Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

7 files changed, 87 insertions, 94 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eedbf422..6f0071a4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -222,7 +222,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
       print "\n";
     end;
     print "install:";
-    if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)";
+    if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
     print "\n";
     if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc;
     if (not_empty cmofiles) then
@@ -291,18 +291,18 @@ let implicit () =
     print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.ml4.d: %.ml4\n";
-    print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml_rules () =
     print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "%.ml.d: %.ml\n";
     print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let cmxs_rules () =
+    print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n";
     print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in
   let mllib_rules () =
     print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n";
     print "%.mllib.d: %.mllib\n";
     print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let mlpack_rules () =
@@ -411,7 +411,7 @@ let parameters () =
   print "# DSTROOT to specify a prefix to install path.\n\n";
   print "# Here is a hack to make $(eval $(shell works:\n";
   print "define donewline\n\n\nendef\n";
-  print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\\n' '@'; })))\n";
+  print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"
 
 let include_dirs (inc_i,inc_r) =
@@ -543,14 +543,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
       classify_files_by_root "CMXSFILES" (l1@l2) inc;
   end;
-  print "\n";
+  print "ifeq '$(HASNATDYNLINK)' 'true'\n";
+  print "HASNATDYNLINK_OR_EMPTY := yes\n";
+  print "else\n";
+  print "HASNATDYNLINK_OR_EMPTY :=\n";
+  print "endif\n\n";
   section "Definition of the toplevel targets.";
   print "all: ";
   if !some_vfile then print "$(VOFILES) ";
   if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) ";
   if !some_mllibfile then print "$(CMAFILES) ";
   if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile
-  then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) ";
+  then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
   print_list "\\\n  " other_targets; print "\n\n";
   if !some_mlifile then
     begin
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml
index 1a9b9c73..350b59aa 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml
@@ -13,15 +13,6 @@
  * Perl isn't as portable as it pretends to be, and is quite difficult
  * to read and maintain... Let us rewrite the stuff in Caml! *)
 
-let _ =
-  match Sys.os_type with
-    | "Unix" -> ()
-    | _ -> begin
-      	print_string "This program only runs under Unix !\n";
-      	flush stdout;
-      	exit 1
-      end
-
 let linelen = ref 72
 let output = ref ""
 let output_specified = ref false
@@ -31,6 +22,7 @@ let verbose = ref false
 let slanted = ref false
 let hrule = ref false
 let small = ref false
+let boot = ref false
 
 let coq_prompt = Str.regexp "Coq < "
 let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
@@ -86,21 +78,23 @@ let bang    = Str.regexp "!"
 let expos   = Str.regexp "^"
 
 let tex_escaped s =
-  let rec trans = parser
-    | [< s1 = (parser
-		 | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] ->
-		     "\\" ^ (String.make 1 c)
-		 | [< ''\\' >] -> "{\\char'134}"
-		 | [< ''^'  >] -> "{\\char'136}"
-		 | [< ''~'  >] -> "{\\char'176}"
-		 | [< '' '  >] -> "~"
-		 | [< ''<'  >] -> "{<}"
-		 | [< ''>'  >] -> "{>}"
-		 | [< 'c >]    -> String.make 1 c);
-	 s2 = trans >] -> s1 ^ s2
-    | [< >] -> ""
+  let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
+  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
+  let adapt_delim = function
+    | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "\\" -> "{\\char'134}"
+    | "^" -> "{\\char'136}"
+    | "~" -> "{\\char'176}"
+    | " " -> "~"
+    | "<" -> "{<}"
+    | ">" -> "{>}"
+    | _ -> assert false
+  in
+  let adapt = function
+    | Str.Text s -> s
+    | Str.Delim s -> adapt_delim s
   in
-  trans (Stream.of_string s)
+  String.concat "" (List.map adapt (Str.full_split delims s))
 
 let encapsule sl c_out s =
   if sl then
@@ -196,11 +190,11 @@ let insert texfile coq_output result =
     else begin
       if !verbose then Printf.printf "Coq < %s\n" s;
       if has_match dot_end_line s then
-       	let bl = next_block (succ k) in
+	let bl = next_block (succ k) in
 	if !verbose then List.iter print_endline bl;
 	eval 0
       else
-       	eval (succ k)
+	eval (succ k)
     end
   in
   try
@@ -266,18 +260,29 @@ let parse_cl () =
 	"-hrule", Arg.Set hrule,
 	"           Coq parts are written between 2 horizontal lines";
 	"-small", Arg.Set small,
-	"           Coq parts are written in small font"
+	"           Coq parts are written in small font";
+	"-boot", Arg.Set boot,
+	"           Launch coqtop with the -boot option"
       ]
       (fun s -> files := s :: !files)
       "coq-tex [options] file ..."
 
+let find_coqtop () =
+  let prog = Sys.executable_name in
+  try
+    let size = String.length prog in
+    let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in
+    (String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7))
+  with Not_found -> begin
+    Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
+    "coqtop"
+  end
+
 let main () =
   parse_cl ();
-  if !image = "" then begin
-    Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
-    image := "coqtop"
-  end;
-  if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin
+  if !image = "" then image := Filename.quote (find_coqtop ());
+  if !boot then image := !image ^ " -boot";
+  if Sys.command (!image ^ " -batch -silent") <> 0 then begin
     Printf.printf "Error: ";
     let _ = Sys.command (!image ^ " -batch") in
     exit 1
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c929e559..4977a94c 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -288,7 +288,7 @@ let canonize f =
     | (f,_) :: _ -> escape f
     | _ -> escape f
 
-let traite_fichier_Coq verbose f =
+let rec traite_fichier_Coq verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
@@ -347,7 +347,9 @@ let traite_fichier_Coq verbose f =
 	        addQueue deja_vu_v [str];
                 try
                   let file_str = Hashtbl.find vKnown [str] in
-                  printf " %s.v" (canonize file_str)
+                  let canon = canonize file_str in
+                  printf " %s.v" canon;
+                  traite_fichier_Coq true (canon ^ ".v")
                 with Not_found -> ()
        	      end
           | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index d319ce72..14447b06 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -35,17 +35,18 @@ type entry_type =
 type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
-  | Mod of coq_module * string
 
 let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-(** [deftable] stores only definitions and is used to interpolate idents
-    inside comments, which are not globalized otherwise. *)
-
+(** [deftable] stores only definitions and is used to build the index *)
 let deftable = Hashtbl.create 97
 
+(** [byidtable] is used to interpolate idents inside comments, which are not
+    globalized otherwise. *)
+let byidtable = Hashtbl.create 97
+
 (** [reftable] stores references and definitions *)
 let reftable = Hashtbl.create 97
 
@@ -59,25 +60,25 @@ let full_ident sp id =
   else ""
 
 let add_def loc1 loc2 ty sp id =
+  let fullid = full_ident sp id in
+  let def = Def (fullid, ty) in
   for loc = loc1 to loc2 do
-    Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+    Hashtbl.add reftable (!current_library, loc) def
   done;
-  Hashtbl.add deftable id (Def (full_ident sp id, ty))
+  Hashtbl.add deftable !current_library (fullid, ty);
+  Hashtbl.add byidtable id (!current_library, fullid, ty)
 
 let add_ref m loc m' sp id ty =
+  let fullid = full_ident sp id in
   if Hashtbl.mem reftable (m, loc) then ()
-  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
   let idx = if id = "<>" then m' else id in
-    if Hashtbl.mem deftable idx then ()
-    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
-  Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable m (Mod (m', id))
+    if Hashtbl.mem byidtable idx then ()
+    else Hashtbl.add byidtable idx (m', fullid, ty)
 
 let find m l = Hashtbl.find reftable (m, l)
 
-let find_string m s = Hashtbl.find deftable s
+let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
 (*s Manipulating path prefixes *)
 
@@ -289,10 +290,7 @@ let all_entries () =
     let l = try Hashtbl.find bt t with Not_found -> [] in
       Hashtbl.replace bt t ((s,m) :: l)
   in
-  let classify m e = match e with
-    | Def (s,t) -> add_g s m t; add_bt t s m
-    | Ref _ | Mod _ -> ()
-  in
+  let classify m (s,t) = (add_g s m t; add_bt t s m) in
     Hashtbl.iter classify deftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global";
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 8c658a90..0f62a086 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -34,10 +34,11 @@ val type_name : entry_type -> string
 type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
-  | Mod of coq_module * string
 
+(* Find what symbol coqtop said is located at loc in the source file *)
 val find : coq_module -> loc -> index_entry
 
+(* Find what data is referred to by some string in some coq module *)
 val find_string : coq_module -> string -> index_entry
 
 val add_module : coq_module -> unit
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index cd33528a..0dc86bc8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -126,9 +126,12 @@ let initialize_texmacs () =
 
 let token_tree_texmacs = ref (initialize_texmacs ())
 
+let token_tree_latex = ref Tokens.empty_ttree
+let token_tree_html = ref Tokens.empty_ttree
+
 let initialize_tex_html () =
   let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
-    List.fold_right (fun (s,l,l') (tt,tt') ->
+  let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') ->
       (Tokens.ttree_add tt s l,
        match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l'))
       [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
@@ -151,10 +154,9 @@ let initialize_tex_html () =
 	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
 	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
 	(* "fun", "\\ensuremath{\\lambda}" ? *)
-      ] (Tokens.empty_ttree,Tokens.empty_ttree)
-
-let token_tree_latex = ref (fst (initialize_tex_html ()))
-let token_tree_html = ref (snd (initialize_tex_html ()))
+      ] (Tokens.empty_ttree,Tokens.empty_ttree) in
+  token_tree_latex := tree_latex;
+  token_tree_html  := tree_html
 
 let add_printing_token s (t1,t2) =
   (match t1 with None -> () | Some t1 ->
@@ -325,9 +327,6 @@ module Latex = struct
       let space = 0.5 *. (float n) in
       printf "\\coqdocindent{%2.2fem}\n" space
 
-  let module_ref m s =
-    printf "\\coqdocmodule{%s}{%s}" m (escaped s)
-
   let ident_ref m fid typ s =
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
@@ -356,12 +355,8 @@ module Latex = struct
   let reference s = function
     | Def (fullid,typ) ->
 	defref (get_module false) fullid typ s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,typ) ->
 	ident_ref m fullid typ s
-    | Mod _ ->
-	printf "\\coqdocvar{%s}" (escaped s)
 
   (*s The sublexer buffers symbol characters and attached
        uninterpreted ident and try to apply special translation such as,
@@ -389,6 +384,7 @@ module Latex = struct
     last_was_in := false
 
   let initialize () =
+    initialize_tex_html ();
     Tokens.token_tree := token_tree_latex;
     Tokens.outfun := output_sublexer_string
 
@@ -534,10 +530,7 @@ module Html = struct
 	end
 
   let trailer () =
-    if !index && (get_module false) <> "Index" then
-      printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
-    if !header_trailer then
-      if !footer_file_spec then
+    if !header_trailer && !footer_file_spec then
 	let cin = Pervasives.open_in !footer_file in
 	  try
 	    while true do
@@ -545,12 +538,14 @@ module Html = struct
 		printf "%s\n" s
 	    done
 	  with End_of_file -> Pervasives.close_in cin
-      else
-	begin
-	  printf "<hr/>This page has been generated by ";
-	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
-	  printf "</div>\n\n</div>\n\n</body>\n</html>"
-	end
+    else
+      begin
+        if !index && (get_module false) <> "Index" then
+          printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
+	printf "<hr/>This page has been generated by ";
+	printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
+	printf "</div>\n\n</div>\n\n</body>\n</html>"
+      end
 
   let start_module () =
     let ln = !lib_name in
@@ -620,15 +615,6 @@ module Html = struct
        | Some n -> n
        | None -> addr)
 
-  let module_ref m s =
-    match find_module m with
-      | Local ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External m when !externals ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External _ | Unknown ->
-	  output_string s
-
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
@@ -645,12 +631,8 @@ module Html = struct
     | Def (fullid,ty) ->
 	printf "<a name=\"%s\">" fullid;
 	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
-    | Mod _ ->
-	printf "<span class=\"id\" type=\"mod\">%s</span>" s
 
   let output_sublexer_string doescape issymbchar tag s =
     let s = if doescape then escaped s else s in
@@ -667,6 +649,7 @@ module Html = struct
     Tokens.output_tagged_symbol_char tag c
 
   let initialize () =
+    initialize_tex_html();
     Tokens.token_tree := token_tree_html;
     Tokens.outfun := output_sublexer_string
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 1e889639..22a36ede 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -21,7 +21,7 @@ let eval_call (call:'a Ide_intf.call) =
   Xml_utils.print_xml (snd !coqtop) xml_query;
   flush (snd !coqtop);
   let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
-  let res = Ide_intf.to_answer xml_answer in
+  let res = Ide_intf.to_answer xml_answer call in
   prerr_endline (Ide_intf.pr_full_value call res);
   match res with Interface.Fail _ -> exit 1 | _ -> ()