Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 134 insertions, 129 deletions

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 177fc2bc..18a44a44 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 8669 2006-03-28 17:34:15Z notin $ i*)
+(*i $Id: main.ml 8777 2006-05-02 10:14:39Z notin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -54,6 +54,7 @@ let usage () =
   prerr_endline "  --no-externals      no links to Coq standard library";
   prerr_endline "  --coqlib <url>      set URL for Coq standard library";
   prerr_endline "                      (default is http://coq.inria.fr/library/)";
+  prerr_endline "  --coqlib_path <dir> set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>   map physical dir to Coq dir";
   prerr_endline "  --latin1            set ISO-8859-1 input language";
   prerr_endline "  --utf8              set UTF-8 input language";
@@ -71,12 +72,12 @@ 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 = 
   match !target_language with
     | HTML -> f ^ ".html"
     | _ -> 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\
@@ -87,11 +88,11 @@ let check_if_file_exists f =
     eprintf "\ncoqdoc: %s: no such file\n" f;
     exit 1
   end
-
+    
 let paths = ref []
-
+  
 let add_path m l = paths := (m,l) :: !paths
-
+  
 let exists_dir dir =
   try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false
 
@@ -99,72 +100,72 @@ let add_rec_path f l =
   let rec traverse abs rel =
     add_path abs rel;
     let dirh = Unix.opendir abs in
-    try
-      while true do
-	let f = Unix.readdir dirh in
-	if f <> "" && f.[0] <> '.' && f <> "CVS" then
-	  let abs' = Filename.concat abs f in
-	  try 
-	    if exists_dir abs' then  traverse abs' (rel ^ "." ^ f)
-	  with Unix.Unix_error _ -> 
-	    ()
-      done
-    with End_of_file ->
-      Unix.closedir dirh
+      try
+	while true do
+	  let f = Unix.readdir dirh in
+	    if f <> "" && f.[0] <> '.' && f <> "CVS" then
+	      let abs' = Filename.concat abs f in
+		try 
+		  if exists_dir abs' then  traverse abs' (rel ^ "." ^ f)
+		with Unix.Unix_error _ -> 
+		  ()
+	done
+      with End_of_file ->
+	Unix.closedir dirh
   in
-  if exists_dir f then traverse f l
+    if exists_dir f then traverse f l
 
 (* turn A/B/C into A.B.C *)
 let make_path = Str.global_replace (Str.regexp "/") ".";;
 
 let coq_module file = 
-(* TODO
- * LEM:
- * We should also remove things like "/./" in the middle of the filename,
- * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
- * to the same file / directory (via symlinks), etc. The best way to do
- * all this would be to use the libc function realpath() on _both_ p and
- * file / f before comparing them.
- *
- * The semantics of realpath() on file symlinks might not be what we
- * want... (But it is what we want on directory symlinks.) So, we would
- * have to cook up our own version of realpath()?
- *
- * Do all target platforms have realpath()?
- *)
+  (* TODO
+   * LEM:
+   * We should also remove things like "/./" in the middle of the filename,
+   * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
+   * to the same file / directory (via symlinks), etc. The best way to do
+   * all this would be to use the libc function realpath() on _both_ p and
+   * file / f before comparing them.
+   *
+   * The semantics of realpath() on file symlinks might not be what we
+   * want... (But it is what we want on directory symlinks.) So, we would
+   * have to cook up our own version of realpath()?
+   *
+   * Do all target platforms have realpath()?
+   *)
   let f = chop_extension file in
-  (* remove leading ./ and any number of slashes after *)
+    (* remove leading ./ and any number of slashes after *)
   let f = Str.replace_first (Str.regexp "^\\./+") "" f in
-  if (Str.string_before f 1) = "/" then
-    (* f is an absolute path. Prefixes must be matched with the beginning of f,
-     * not prepended
-     *)
-    let rec trypath = function
-     | [] -> make_path f
-     | (p, lg) :: r ->
-         (* make sure p ends with a single '/'
-          * This guarantees that we don't match a file whose name is
-          * of the form p ^ "foo". It means we may miss p itself,
-          * but this does not matter: coqdoc doesn't do anything
-          * of a directory anyway. *)
-         let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
-         let p_quoted = (Str.quote p) in
-         if (Str.string_match (Str.regexp p_quoted) f 0) then
-           make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
-        else
-           trypath r
-    in trypath !paths
-  else (* f is a relative path *)
-    let rec trypath = function
-      | [] -> 
-	  make_path f
-      | (p,lg) :: r ->
-	  let p_file = Filename.concat p file in
-	  if Sys.file_exists p_file then
-	    make_path (Filename.concat lg f)
-	  else
-	    trypath r
-    in trypath !paths;;
+    if (Str.string_before f 1) = "/" then
+      (* f is an absolute path. Prefixes must be matched with the beginning of f,
+       * not prepended
+       *)
+      let rec trypath = function
+	| [] -> make_path f
+	| (p, lg) :: r ->
+            (* make sure p ends with a single '/'
+             * This guarantees that we don't match a file whose name is
+             * of the form p ^ "foo". It means we may miss p itself,
+             * but this does not matter: coqdoc doesn't do anything
+             * of a directory anyway. *)
+            let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
+            let p_quoted = (Str.quote p) in
+              if (Str.string_match (Str.regexp p_quoted) f 0) then
+		make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
+              else
+		trypath r
+      in trypath !paths
+    else (* f is a relative path *)
+      let rec trypath = function
+	| [] -> 
+	    make_path f
+	| (p,lg) :: r ->
+	    let p_file = Filename.concat p file in
+	      if Sys.file_exists p_file then
+		make_path (Filename.concat lg f)
+	      else
+		trypath r
+      in trypath !paths;;
 
 let what_file f =
   check_if_file_exists f;
@@ -176,43 +177,43 @@ let what_file f =
     eprintf "\ncoqdoc: don't know what to do with %s\n" f;
     exit 1
   end
-
+    
 (*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
-    in the file named [f]. These file names must be separated by spaces,
-    tabulations or newlines.
+ *  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
+ *  in the file named [f]. These file names must be separated by spaces,
+ *  tabulations or newlines.
  *)
 
 let files_from_file f =
   let files_from_channel ch =
     let buf = Buffer.create 80 in
     let l = ref [] in
-    try
-      while true do
-	match input_char ch with
-	  | ' ' | '\t' | '\n' ->
-	      if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
-	      Buffer.clear buf
-	  | c -> 
-	      Buffer.add_char buf c
-      done; []
-    with End_of_file ->
-      List.rev !l
+      try
+	while true do
+	  match input_char ch with
+	    | ' ' | '\t' | '\n' ->
+		if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
+		Buffer.clear buf
+	    | c -> 
+		Buffer.add_char buf c
+	done; []
+      with End_of_file ->
+	List.rev !l
   in
-  try
-    check_if_file_exists f;
-    let ch = open_in f in
-    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;
-    exit 1
-  end
-
+    try
+      check_if_file_exists f;
+      let ch = open_in f in
+      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;
+      exit 1
+    end
+      
 (*s \textbf{Parsing of the command line.} *)
-
+      
 let output_file = ref ""
 let dvi = ref false
 let ps = ref false
@@ -222,9 +223,9 @@ let parse () =
   let add_file f = files := f :: !files in
   let rec parse_rec = function
     | [] -> ()
-
+	
     | ("-nopreamble" | "--nopreamble" | "--no-preamble"
-    |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
+      |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
 	header_trailer := false; parse_rec rem
     | ("-p" | "--preamble") :: s :: rem ->
 	push_in_preamble s; parse_rec rem
@@ -239,7 +240,7 @@ let parse () =
     | ("-stdout" | "--stdout") :: rem ->
 	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
-	out_to := File f; parse_rec rem
+	out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
     | ("-o" | "--output") :: [] -> 
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
@@ -280,10 +281,10 @@ let parse () =
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
 	Cdglobals.set_utf8 (); parse_rec rem
-
+	  
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
-
+	  
     | ("-h" | "-help" | "-?" | "--help") :: rem ->
 	banner (); usage ()
     | ("-v" | "-version" | "--version") :: _ ->
@@ -317,13 +318,17 @@ let parse () =
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
+    | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
+	Cdglobals.coqlib_path := d; parse_rec rem
+    | ("--coqlib_path" | "-coqlib_path") :: [] ->
+	usage ()
     | f :: rem -> 
 	add_file (what_file f); parse_rec rem
   in 
-  parse_rec (List.tl (Array.to_list Sys.argv));
-  List.rev !files
-
+    parse_rec (List.tl (Array.to_list Sys.argv));
+    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]. 
     If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
@@ -331,41 +336,41 @@ let parse () =
 
 let locally dir f x =
   let cwd = Sys.getcwd () in
-  try
-    Sys.chdir dir; let y = f x in Sys.chdir cwd; y
-  with e ->
-    Sys.chdir cwd; raise e
+    try
+      Sys.chdir dir; let y = f x in Sys.chdir cwd; y
+    with e ->
+      Sys.chdir cwd; raise e
 
 let clean_temp_files basefile =
   let remove f = try Sys.remove f with _ -> () in
-  remove (basefile ^ ".tex");
-  remove (basefile ^ ".log");
-  remove (basefile ^ ".aux");
-  remove (basefile ^ ".dvi");
-  remove (basefile ^ ".ps");
-  remove (basefile ^ ".haux");
-  remove (basefile ^ ".html")
-
+    remove (basefile ^ ".tex");
+    remove (basefile ^ ".log");
+    remove (basefile ^ ".aux");
+    remove (basefile ^ ".dvi");
+    remove (basefile ^ ".ps");
+    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
-    while true do print_char (input_char c) done
-  with End_of_file ->
-    close_in c
+    try
+      while true do print_char (input_char c) done
+    with End_of_file ->
+      close_in c
 
 let copy src dst =
   let cin = open_in src 
   and 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
+    try
+      while true do Pervasives.output_char cout (input_char cin) done
+    with End_of_file ->
+      close_in cin; close_out cout
 
 
 (*s Functions for generating output files *)
-
+	
 let gen_one_file l =
   let file = function
     | Vernac_file (f,m) -> 
@@ -416,15 +421,15 @@ let gen_mult_files l =
 let index_module = function
   | Vernac_file (_,m) -> Index.add_module m
   | Latex_file _ -> ()
-
+      
 let produce_document l =
   List.iter index_module l;
   (if !target_language=HTML then
-    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in
+    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
       copy src dst);
   (if !target_language=LaTeX then
-    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in
+    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
@@ -439,7 +444,7 @@ let produce_document l =
 	close_out_file()
     | MultFiles ->
 	gen_mult_files l
-
+	  
 let produce_output fl =
   if not (!dvi || !ps) then begin
     produce_document fl
@@ -493,7 +498,7 @@ let produce_output fl =
 
 let main () =
   let files = parse () in
-  if not !quiet then banner ();
-  if files <> [] then produce_output files
-
+    if not !quiet then banner ();
+    if files <> [] then produce_output files
+      
 let _ = Printexc.catch main ()