Added checksums to glob files and warned about possibly missing

packages for utf8.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 37 insertions, 9 deletions

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";