Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 156 insertions, 124 deletions

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2ee9ac96..67c63865 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -46,6 +46,7 @@ let usage () =
   prerr_endline "  --with-footer <file> append <file> as html footer";
   prerr_endline "  --no-index           do not output the index";
   prerr_endline "  --multi-index        index split in multiple files";
+  prerr_endline "  --index <string>     set index name (default is index)";
   prerr_endline "  --toc                output a table of contents";
   prerr_endline "  --vernac <file>      consider <file> as a .v file";
   prerr_endline "  --tex <file>         consider <file> as a .tex file";
@@ -53,8 +54,9 @@ let usage () =
   prerr_endline "  --files-from <file>  read file names to process in <file>";
   prerr_endline "  --glob-from <file>   read globalization information from <file>";
   prerr_endline "  --quiet              quiet mode (default)";
-  prerr_endline "  --verbose            verbose mode";  
+  prerr_endline "  --verbose            verbose mode";
   prerr_endline "  --no-externals       no links to Coq standard library";
+  prerr_endline "  --external <url> <d> set URL for external library d";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
   prerr_endline ("                       (default is " ^ Coq_config.wwwstdlib ^ ")");
   prerr_endline "  --boot               run in boot mode";
@@ -66,6 +68,11 @@ let usage () =
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
   prerr_endline "  --parse-comments     parse regular comments";
+  prerr_endline "  --plain-comments     consider comments as non-literate text";
+  prerr_endline "  --toc-depth <int>    don't include TOC entries for sections below level <int>";
+  prerr_endline "  --no-lib-name        don't display \"Library\" before library names in the toc";
+  prerr_endline "  --lib-name <string>  call top level toc entries <string> instead of \"Library\"";
+  prerr_endline "  --lib-subtitles      first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles";
   prerr_endline "";
   exit 1
 
@@ -74,20 +81,20 @@ let obsolete s =
 
 (*s \textbf{Banner.} Always printed. Notice that it is printed on error
     output, so that when the output of [coqdoc] is redirected this header
-    is not (unless both standard and error outputs are redirected, of 
+    is not (unless both standard and error outputs are redirected, of
     course). *)
 
 let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
     Coq_config.version Coq_config.compile_date;
   flush stderr
-    
-let target_full_name f = 
+
+let target_full_name f =
   match !Cdglobals.target_language with
     | HTML -> f ^ ".html"
     | Raw -> f ^ ".txt"
     | _ -> f ^ ".tex"
-	
+
 (*s \textbf{Separation of files.} Files given on the command line are
     separated according to their type, which is determined by their
     suffix.  Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
@@ -95,12 +102,12 @@ let target_full_name f =
 
 let check_if_file_exists f =
   if not (Sys.file_exists f) then begin
-    eprintf "\ncoqdoc: %s: no such file\n" f;
+    eprintf "coqdoc: %s: no such file\n" f;
     exit 1
   end
 
 
-(*s Manipulations of paths and path aliases *) 
+(*s Manipulations of paths and path aliases *)
 
 let normalize_path p =
   (* We use the Unix subsystem to normalize a physical path (relative
@@ -109,50 +116,43 @@ let normalize_path p =
      works... *)
   (* Rq: Sys.getcwd () returns paths without '/' at the end *)
   let orig = Sys.getcwd () in
-    Sys.chdir p;
-    let res = Sys.getcwd () in
-      Sys.chdir orig; 
-      res
+  Sys.chdir p;
+  let res = Sys.getcwd () in
+  Sys.chdir orig;
+  res
 
 let normalize_filename f =
   let basename = Filename.basename f in
   let dirname = Filename.dirname f in
-    Filename.concat (normalize_path dirname) basename
+  normalize_path dirname, basename
 
 (* [paths] maps a physical path to a name *)
 let paths = ref []
-  
-let add_path dir name = 
-  (* if dir is relative we add both the relative and absolute name *)
+
+let add_path dir name =
   let p = normalize_path dir in
-    paths := (p,name) :: !paths
-  
-(* turn A/B/C into A.B.C *)
-let name_of_path = Str.global_replace (Str.regexp "/") ".";;
+  paths := (p,name) :: !paths
 
-let coq_module filename = 
+(* turn A/B/C into A.B.C *)
+let rec name_of_path p name dirname suffix =
+  if p = dirname then String.concat "." (name::suffix)
+  else
+    let subdir = Filename.dirname dirname in
+    if subdir = dirname then raise Not_found
+    else name_of_path p name subdir (Filename.basename dirname::suffix)
+
+let coq_module filename =
   let bfname = Filename.chop_extension filename in
-  let nfname = normalize_filename bfname in
-  let rec change_prefix map f = 
-    match map with
-      | [] -> 
-	  (* There is no prefix alias; 
-	     we just cut the name wrt current working directory *)
-	  let cwd = Sys.getcwd () in
-	  let exp = Str.regexp (Str.quote (cwd ^ "/")) in
-	    if (Str.string_match exp f 0) then
-	      name_of_path (Str.replace_first exp "" f)
-	    else
-	      name_of_path f
-      | (p, name) :: rem ->
-          let expp = Str.regexp (Str.quote p) in
-	    if (Str.string_match expp f 0) then
-	      let newp = Str.replace_first expp name f in
-		name_of_path newp
-            else
-	      change_prefix rem f
+  let dirname, fname = normalize_filename bfname in
+  let rec change_prefix = function
+    (* Follow coqc: if in scope of -R, substitute logical name *)
+    (* otherwise, keep only base name *)
+    | [] -> fname
+    | (p, name) :: rem ->
+	try name_of_path p name dirname [fname]
+	with Not_found -> change_prefix rem
   in
-    change_prefix !paths nfname
+  change_prefix !paths
 
 let what_file f =
   check_if_file_exists f;
@@ -160,10 +160,10 @@ let what_file f =
     Vernac_file (f, coq_module f)
   else if Filename.check_suffix f ".tex" then
     Latex_file f
-  else 
+  else
      (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
-    
-(*s \textbf{Reading file names from a file.} 
+
+(*s \textbf{Reading file names from a file.}
  *  File names may be given
  *  in a file instead of being given on the command
  *  line. [(files_from_file f)] returns the list of file names contained
@@ -181,7 +181,7 @@ let files_from_file f =
 	    | ' ' | '\t' | '\n' ->
 		if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
 		Buffer.clear buf
-	    | c -> 
+	    | c ->
 		Buffer.add_char buf c
 	done; []
       with End_of_file ->
@@ -193,12 +193,12 @@ let files_from_file f =
       let l = files_from_channel ch in
 	close_in ch;l
     with Sys_error s -> begin
-      eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
+      eprintf "coqdoc: cannot read from file %s (%s)\n" f s;
       exit 1
     end
-      
+
 (*s \textbf{Parsing of the command line.} *)
-      
+
 let dvi = ref false
 let ps = ref false
 let pdf = ref false
@@ -208,7 +208,7 @@ let parse () =
   let add_file f = files := f :: !files in
   let rec parse_rec = function
     | [] -> ()
-	
+
     | ("-nopreamble" | "--nopreamble" | "--no-preamble"
       |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
 	header_trailer := false; parse_rec rem
@@ -228,17 +228,21 @@ let parse () =
 	index := false; parse_rec rem
     | ("-multi-index" | "--multi-index") :: rem ->
 	multi_index := true; parse_rec rem
+    | ("-index" | "--index") :: s :: rem ->
+	Cdglobals.index_name := s; parse_rec rem
+    | ("-index" | "--index") :: [] ->
+	usage ()
     | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
 	toc := true; parse_rec rem
     | ("-stdout" | "--stdout") :: rem ->
 	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
 	out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
-    | ("-o" | "--output") :: [] -> 
+    | ("-o" | "--output") :: [] ->
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
 	output_dir := dir; parse_rec rem
-    | ("-d" | "--directory") :: [] -> 
+    | ("-d" | "--directory") :: [] ->
 	usage ()
     | ("-s" | "--short") :: rem ->
 	short := true; parse_rec rem
@@ -276,39 +280,60 @@ let parse () =
 	Cdglobals.raw_comments := true; parse_rec rem
     | ("-parse-comments" | "--parse-comments") :: rem ->
 	Cdglobals.parse_comments := true; parse_rec rem
+    | ("-plain-comments" | "--plain-comments") :: rem ->
+	Cdglobals.plain_comments := true; parse_rec rem
     | ("-interpolate" | "--interpolate") :: rem ->
 	Cdglobals.interpolate := true; parse_rec rem
+    | ("-toc-depth" | "--toc-depth") :: [] ->
+      usage ()
+    | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
+      let d = try int_of_string ds with
+                Failure _ ->
+                  (eprintf "--toc-depth must be followed by an integer\n";
+                   exit 1)
+      in
+      Cdglobals.toc_depth := Some d;
+      parse_rec rem
+    | ("-no-lib-name" | "--no-lib-name") :: rem ->
+      Cdglobals.lib_name := "";
+      parse_rec rem
+    | ("-lib-name" | "--lib-name") :: ds :: rem ->
+      Cdglobals.lib_name := ds;
+      parse_rec rem
+    | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
+      Cdglobals.lib_subtitles := true;
+      parse_rec rem
 
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
 	Cdglobals.set_utf8 (); parse_rec rem
-	  
+
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
     | ("-v" | "-verbose" | "--verbose") :: rem ->
 	quiet := false; parse_rec rem
-	  
+
     | ("-h" | "-help" | "-?" | "--help") :: rem ->
 	banner (); usage ()
     | ("-V" | "-version" | "--version") :: _ ->
 	banner (); exit 0
 
-    | ("-vernac-file" | "--vernac-file") :: f :: rem -> 
+    | ("-vernac-file" | "--vernac-file") :: f :: rem ->
 	check_if_file_exists f;
 	add_file (Vernac_file (f, coq_module f)); parse_rec rem
     | ("-vernac-file" | "--vernac-file") :: [] ->
 	usage ()
-    | ("-tex-file" | "--tex-file") :: f :: rem -> 
+    | ("-tex-file" | "--tex-file") :: f :: rem ->
 	add_file (Latex_file f); parse_rec rem
     | ("-tex-file" | "--tex-file") :: [] ->
 	usage ()
     | ("-files" | "--files" | "--files-from") :: f :: rem ->
-	List.iter (fun f -> add_file (what_file f)) (files_from_file f); 
+	List.iter (fun f -> add_file (what_file f)) (files_from_file f);
 	parse_rec rem
     | ("-files" | "--files") :: [] ->
 	usage ()
-    | "-R" :: path :: log :: rem -> 
+    | "-R" :: path :: log :: rem ->
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
 	usage ()
@@ -318,6 +343,8 @@ let parse () =
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
 	Cdglobals.externals := false; parse_rec rem
+    | ("--external" | "-external") :: u :: logicalpath :: rem ->
+	Index.add_external_library logicalpath u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: u :: rem ->
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
@@ -328,16 +355,15 @@ let parse () =
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
 	usage ()
-    | f :: rem -> 
+    | f :: rem ->
 	add_file (what_file f); parse_rec rem
-  in 
+  in
     parse_rec (List.tl (Array.to_list Sys.argv));
-    Output.initialize ();
     List.rev !files
 
-      
+
 (*s The following function produces the output. The default output is
-    the \LaTeX\ document: in that case, we just call [Web.produce_document]. 
+    the \LaTeX\ document: in that case, we just call [Web.produce_document].
     If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
     we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
 
@@ -359,9 +385,9 @@ let clean_temp_files basefile =
     remove (basefile ^ ".pdf");
     remove (basefile ^ ".haux");
     remove (basefile ^ ".html")
-      
+
 let clean_and_exit file res = clean_temp_files file; exit res
-  
+
 let cat file =
   let c = open_in file in
     try
@@ -370,20 +396,26 @@ let cat file =
       close_in c
 
 let copy src dst =
-  let cin = open_in src 
-  and cout = open_out dst in
+  let cin = open_in src in
+  try
+    let cout = open_out dst in
     try
       while true do Pervasives.output_char cout (input_char cin) done
     with End_of_file ->
-      close_in cin; close_out cout
-
+      close_out cout;
+      close_in cin
+  with Sys_error e ->
+    eprintf "%s\n" e;
+    exit 1
 
 (*s Functions for generating output files *)
 
 let gen_one_file l =
   let file = function
-    | Vernac_file (f,m) -> 
-	Output.set_module m; Pretty.coq_file f m
+    | Vernac_file (f,m) ->
+        let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
+          Output.set_module m sub;
+          Cpretty.coq_file f m
     | Latex_file _ -> ()
   in
     if (!header_trailer) then Output.header ();
@@ -391,74 +423,73 @@ let gen_one_file l =
     List.iter file l;
     if !index then Output.make_index();
     if (!header_trailer) then Output.trailer ()
-      
+
 let gen_mult_files l =
   let file = function
-    | Vernac_file (f,m) -> 
-	Output.set_module m;
+    | Vernac_file (f,m) ->
+      let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
 	let hf = target_full_name m in
+        Output.set_module m sub;
 	  open_out_file hf;
-	  if (!header_trailer) then Output.header (); 
-	  Pretty.coq_file f m; 
+	  if (!header_trailer) then Output.header ();
+	  Cpretty.coq_file f m;
 	  if (!header_trailer) then Output.trailer ();
 	  close_out_file()
     | Latex_file _ -> ()
   in
     List.iter file l;
     if (!index && !target_language=HTML) then begin
-      if (!multi_index) then Output.make_multi_index (); 
-      open_out_file "index.html"; 
+      if (!multi_index) then Output.make_multi_index ();
+      open_out_file (!index_name^".html");
       page_title := (if !title <> "" then !title else "Index");
-      if (!header_trailer) then Output.header (); 
-      Output.make_index (); 
+      if (!header_trailer) then Output.header ();
+      Output.make_index ();
       if (!header_trailer) then Output.trailer ();
       close_out_file()
     end;
     if (!toc && !target_language=HTML) then begin
-      open_out_file "toc.html"; 
+      open_out_file "toc.html";
       page_title := (if !title <> "" then !title else "Table of contents");
       if (!header_trailer) then Output.header ();
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
-      Output.make_toc (); 
+      Output.make_toc ();
       if (!header_trailer) then Output.trailer ();
       close_out_file()
-    end 
+    end
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
-let read_glob x =
-  match x with
-    | Vernac_file (f,m) ->   
-	let glob = (Filename.chop_extension f) ^ ".glob" in
- 	  (try
-	      Vernac_file (f, Index.read_glob glob)
-            with e -> 
-              eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
-	      x)
-  | Latex_file _ -> x
+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_of = function
+  | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+  | Latex_file _ -> ()
 
 let index_module = function
-  | Vernac_file (f,m) ->   
+  | Vernac_file (f,m) ->
       Index.add_module m
   | Latex_file _ -> ()
-      
+
+let copy_style_file file =
+  let src =
+    List.fold_left
+      Filename.concat !Cdglobals.coqlib_path ["tools";"coqdoc";file] in
+  let dst = coqdoc_out file in
+  if Sys.file_exists src then copy src dst
+  else eprintf "Warning: file %s does not exist\n" src
+
 let produce_document l =
-  (if !target_language=HTML then
-    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
-    let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
-      if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
-  (if !target_language=LaTeX then
-      let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
-      let dst = if !output_dir <> "" then 
-	  Filename.concat !output_dir "coqdoc.sty" 
-	else "coqdoc.sty" in
-	if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
+  if !target_language=HTML then copy_style_file "coqdoc.css";
+  if !target_language=LaTeX then copy_style_file "coqdoc.sty";
   (match !Cdglobals.glob_source with
     | NoGlob -> ()
-    | DotGlob -> ignore (List.map read_glob l)
-    | GlobFile f -> ignore (Index.read_glob f));
+    | DotGlob -> List.iter read_glob_file_of l
+    | GlobFile f -> read_glob_file f);
   List.iter index_module l;
   match !out_to with
-    | StdOut -> 
+    | StdOut ->
 	Cdglobals.out_channel := stdout;
 	gen_one_file l
     | File f ->
@@ -467,11 +498,11 @@ let produce_document l =
 	close_out_file()
     | MultFiles ->
 	gen_mult_files l
-	  
+
 let produce_output fl =
-  if not (!dvi || !ps || !pdf) then 
+  if not (!dvi || !ps || !pdf) then
     produce_document fl
-  else 
+  else
     begin
       let texfile = Filename.temp_file "coqdoc" ".tex" in
       let basefile = Filename.chop_suffix texfile ".tex" in
@@ -479,52 +510,52 @@ let produce_output fl =
 	out_to := File texfile;
 	output_dir := (Filename.dirname texfile);
 	produce_document fl;
-	
+
 	let latexexe = if !pdf then "pdflatex" else "latex" in
-	let latexcmd = 
+	let latexcmd =
 	  let file = Filename.basename texfile in
-	  let file = 
-	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	  let file =
+	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
 	  in
 	    sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
 	in
 	let res = locally (Filename.dirname texfile) Sys.command latexcmd in
 	  if res <> 0 then begin
-	      eprintf "Couldn't run LaTeX successfully\n"; 
+	      eprintf "Couldn't run LaTeX successfully\n";
 	      clean_and_exit basefile res
 	    end;
-	  
+
 	  let dvifile = basefile ^ ".dvi" in
-	    if !dvi then 
+	    if !dvi then
 	      begin
 		match final_out_to with
 		  | MultFiles | StdOut -> cat dvifile
 		  | File f -> copy dvifile f
 	      end;
 	  let pdffile = basefile ^ ".pdf" in
-	    if !pdf then 
+	    if !pdf then
             begin
 	        match final_out_to with
 		  | MultFiles | StdOut -> cat pdffile
 		  | File f -> copy pdffile f
 	    end;
 	    if !ps then begin
-	        let psfile = basefile ^ ".ps" 
+	        let psfile = basefile ^ ".ps"
 		in
-		let command = 
-		  sprintf "dvips %s -o %s %s" dvifile psfile 
+		let command =
+		  sprintf "dvips %s -o %s %s" dvifile psfile
 		    (if !quiet then "> /dev/null 2>&1" else "")
 		in
 		let res = Sys.command command in
 		  if res <> 0 then begin
-		      eprintf "Couldn't run dvips successfully\n"; 
+		      eprintf "Couldn't run dvips successfully\n";
 		      clean_and_exit basefile res
 		    end;
 		  match final_out_to with
 		    | MultFiles | StdOut -> cat psfile
 		    | File f -> copy psfile f
 	      end;
-	 
+
 	    clean_temp_files basefile
     end
 
@@ -534,7 +565,8 @@ let produce_output fl =
 
 let main () =
   let files = parse () in
+    Index.init_coqlib_library ();
     if not !quiet then banner ();
     if files <> [] then produce_output files
-      
+
 let _ = Printexc.catch main ()