aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/dumpglob.ml19
-rw-r--r--interp/dumpglob.mli4
-rw-r--r--tools/coqdoc/index.ml21
-rw-r--r--tools/coqdoc/index.mli2
-rw-r--r--tools/coqdoc/main.ml12
-rw-r--r--tools/coqdoc/output.ml11
-rw-r--r--toplevel/vernac.ml19
7 files changed, 66 insertions, 22 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 26f4d4e19..4a8756b88 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -31,8 +31,6 @@ let noglob () = glob_output := NoGlob
let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
-let multi_dump () = !glob_output = MultFiles
-
let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
@@ -40,6 +38,23 @@ let dump_into_file f = glob_output := File f; open_glob_file f
let dump_string s =
if dump () then Pervasives.output_string !glob_file s
+let start_dump_glob vfile =
+ match !glob_output with
+ | MultFiles ->
+ open_glob_file (Filename.chop_extension vfile ^ ".glob");
+ output_string !glob_file "DIGEST ";
+ output_string !glob_file (Digest.to_hex (Digest.file vfile));
+ output_char !glob_file '\n'
+ | File f ->
+ open_glob_file f;
+ output_string !glob_file "DIGEST NO\n"
+ | NoGlob | StdOut ->
+ ()
+
+let end_dump_glob () =
+ match !glob_output with
+ | MultFiles | File _ -> close_glob_file ()
+ | NoGlob | StdOut -> ()
let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index c8f19ead0..b02cc9669 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -9,8 +9,10 @@
val open_glob_file : string -> unit
val close_glob_file : unit -> unit
+val start_dump_glob : string -> unit
+val end_dump_glob : unit -> unit
+
val dump : unit -> bool
-val multi_dump : unit -> bool
val noglob : unit -> unit
val dump_to_stdout : unit -> unit
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index dbb0c1d6b..2ff0fad70 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -321,8 +321,27 @@ let type_of_string = function
| "sec" -> Section
| s -> raise (Invalid_argument ("type_of_string:" ^ s))
-let read_glob f =
+let ill_formed_glob_file f =
+ eprintf "Warning: ill-formed file %s (links will not be available)\n" f
+let outdated_glob_file f =
+ eprintf "Warning: %s not consistent with corresponding .v file (links will not be available)\n" f
+
+let correct_file vfile f c =
+ let s = input_line c in
+ if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then
+ (ill_formed_glob_file f; false)
+ else
+ let s = String.sub s 7 (String.length s - 7) in
+ match vfile, s with
+ | None, "NO" -> true
+ | Some _, "NO" -> ill_formed_glob_file f; false
+ | None, _ -> ill_formed_glob_file f; false
+ | Some vfile, s ->
+ s = Digest.to_hex (Digest.file vfile) || (outdated_glob_file f; false)
+
+let read_glob vfile f =
let c = open_in f in
+ if correct_file vfile f c then
let cur_mod = ref "" in
try
while true do
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index a5430f5f1..bb775d261 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -52,7 +52,7 @@ val add_external_library : string -> coq_module -> unit
(*s Read globalizations from a file (produced by coqc -dump-glob) *)
-val read_glob : string -> unit
+val read_glob : Digest.t option -> string -> unit
(*s Indexes *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 7dc2c3bf2..b1303f18f 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -447,13 +447,13 @@ let gen_mult_files l =
end
(* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
-let read_glob_file x =
- try Index.read_glob x
- with Sys_error s ->
- eprintf "Warning: %s (links will not be available)\n" s
+let read_glob_file vfile f =
+ try Index.read_glob vfile f
+ with Sys_error s -> eprintf "Warning: %s (links will not be available)\n" s
let read_glob_file_of = function
- | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+ | Vernac_file (f,_) ->
+ read_glob_file (Some f) (Filename.chop_extension f ^ ".glob")
| Latex_file _ -> ()
let index_module = function
@@ -475,7 +475,7 @@ let produce_document l =
(match !Cdglobals.glob_source with
| NoGlob -> ()
| DotGlob -> List.iter read_glob_file_of l
- | GlobFile f -> read_glob_file f);
+ | GlobFile f -> read_glob_file None f);
List.iter index_module l;
match !out_to with
| StdOut ->
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 605196d6f..28cd79968 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -177,11 +177,20 @@ module Latex = struct
let push_in_preamble s = Queue.add s preamble
+ let utf8x_extra_support () =
+ printf "\n";
+ printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
+ printf "%%interpret utf8 characters but extra packages might have to be added\n";
+ printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
+ printf "%%Use coqdoc's option -p to add new packages.\n";
+ printf "\\usepackage{tipa}\n";
+ printf "\n"
+
let header () =
if !header_trailer then begin
printf "\\documentclass[12pt]{report}\n";
if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
- if !inputenc = "utf8x" then printf "\\usepackage{tipa}\n";
+ if !inputenc = "utf8x" then utf8x_extra_support ();
printf "\\usepackage[T1]{fontenc}\n";
printf "\\usepackage{fullpage}\n";
printf "\\usepackage{coqdoc}\n";
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 87e0ebe17..934cddb4f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -307,15 +307,14 @@ let load_vernac verb file =
(* Compile a vernac file (f is assumed without .v suffix) *)
let compile verbosely f =
let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
- if Dumpglob.multi_dump () then
- Dumpglob.open_glob_file (f ^ ".glob");
- Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
- if !Flags.xml_export then !xml_start_library ();
- let _ = load_vernac verbosely long_f_dot_v in
- if Pfedit.get_all_proof_names () <> [] then
- (message "Error: There are pending proofs"; exit 1);
- if !Flags.xml_export then !xml_end_library ();
- if Dumpglob.multi_dump () then Dumpglob.close_glob_file ();
- Library.save_library_to ldir (long_f_dot_v ^ "o")
+ Dumpglob.start_dump_glob long_f_dot_v;
+ Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+ if !Flags.xml_export then !xml_start_library ();
+ let _ = load_vernac verbosely long_f_dot_v in
+ if Pfedit.get_all_proof_names () <> [] then
+ (message "Error: There are pending proofs"; exit 1);
+ if !Flags.xml_export then !xml_end_library ();
+ Dumpglob.end_dump_glob ();
+ Library.save_library_to ldir (long_f_dot_v ^ "o")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 00:57:18 +0000