better documentation regarding user-edition of PVS files

parent ee62f36f
...@@ -1458,7 +1458,8 @@ doc/bnf: doc/bnf.mll ...@@ -1458,7 +1458,8 @@ doc/bnf: doc/bnf.mll
$(OCAMLOPT) -o $@ doc/bnf.ml $(OCAMLOPT) -o $@ doc/bnf.ml
DOC = api glossary ide intro library macros manpages install coq_tactic \ DOC = api glossary ide intro library macros manpages install coq_tactic \
realizations manual starting syntax syntaxref technical version whyml realizations manual starting syntax syntaxref technical version whyml \
pvs
DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC))) DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
......
...@@ -29,8 +29,10 @@ realization: ...@@ -29,8 +29,10 @@ realization:
\texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}. \texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}.
\item insert anything between generated declarations, such as a lemma, \item insert anything between generated declarations, such as a lemma,
an extra definition for the purpose of a proof, etc. an extra definition for the purpose of a proof, an extra
\texttt{IMPORTING} command, etc. Do not forget to surround these
extra declarations with blank lines.
\end{itemize} \end{itemize}
\why makes some effort to merge the new declarations with the old ones \why makes some effort to merge new declarations with old ones
and with the user chunks. If it happens that some chunks could not be and with user chunks. If it happens that some chunks could not be
merged, they are appended at the end of the file, in comments. merged, they are appended at the end of the file, in comments.
...@@ -886,7 +886,9 @@ let print_task printer_args realize ?old fmt task = ...@@ -886,7 +886,9 @@ let print_task printer_args realize ?old fmt task =
let lib = if path = thpath then "" else String.concat "." path ^ "@" in let lib = if path = thpath then "" else String.concat "." path ^ "@" in
fprintf fmt "IMPORTING %s%s@\n" lib th.Theory.th_name.id_string) fprintf fmt "IMPORTING %s%s@\n" lib th.Theory.th_name.id_string)
realized_theories; realized_theories;
fprintf fmt "%% do not edit above this line@\n@\n"; fprintf fmt "%% do not edit above this line@\n";
fprintf fmt
"%% surround new declarations you insert below with blank lines@\n@\n";
print_decls ~old info fmt local_decls; print_decls ~old info fmt local_decls;
output_remaining fmt !old; output_remaining fmt !old;
fprintf fmt "@]@\nEND %s@\n@]" thname fprintf fmt "@]@\nEND %s@\n@]" thname
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment