Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

3 files changed, 33 insertions, 15 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 44b9bd3c..3339b1db 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -32,6 +32,13 @@ let open_out_file f =
 let close_out_file () = close_out !out_channel
 
 
+type glob_source_t =
+    | NoGlob
+    | DotGlob
+    | GlobFile of string
+
+let glob_source = ref DotGlob 
+
 let header_trailer = ref true
 let header_file = ref ""
 let header_file_spec = ref false
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 7111187f..81560259 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 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: main.ml 11236 2008-07-18 15:58:12Z notin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -50,6 +50,7 @@ let usage () =
   prerr_endline "  --tex <file>         consider <file> as a .tex file";
   prerr_endline "  -p <string>          insert <string> in LaTeX preamble";
   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 "  --no-externals       no links to Coq standard library";
@@ -300,7 +301,7 @@ let parse () =
     | "-R" :: ([] | [_]) ->
 	usage ()
     | ("-glob-from" | "--glob-from") :: f :: rem ->
-	obsolete "glob-from"; parse_rec rem
+	glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
@@ -436,7 +437,10 @@ let produce_document l =
 	  Filename.concat !output_dir "coqdoc.sty" 
 	else "coqdoc.sty" in
 	copy src dst);
-  let l = List.map read_glob l in
+  (match !Cdglobals.glob_source with
+    | NoGlob -> ()
+    | DotGlob -> ignore (List.map read_glob l)
+    | GlobFile f -> ignore (Index.read_glob f));
   List.iter index_module l;
   match !out_to with
     | StdOut -> 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 8be3e0b0..baace5ba 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 11154 2008-06-19 18:42:19Z msozeau $ i*)
+(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -56,6 +56,7 @@
 
   let formatted = ref false
   let brackets = ref 0
+  let comment_level = ref 0
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -93,7 +94,8 @@
 
   let reset () =
     formatted := false;
-    brackets := 0
+    brackets := 0;
+    comment_level := 0
 
   (* erasing of Section/End *)
 
@@ -385,6 +387,7 @@ rule coq_bol = parse
   | space* "(**" space+ "printing" space+
       { eprintf "warning: bad 'printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
+	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+ 
@@ -394,10 +397,12 @@ rule coq_bol = parse
   | space* "(**" space+ "remove" space+ "printing" space+
       { eprintf "warning: bad 'remove printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
+	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(*"
-      { let eol = comment lexbuf in
+      { comment_level := 1; 
+	let eol = comment lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
       { () }
@@ -421,7 +426,8 @@ and coq = parse
 	  Output.end_doc (); Output.start_coq (); 
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
-      { let eol = comment lexbuf in
+      { comment_level := 1;
+	let eol = comment lexbuf in
 	  if eol then begin Output.line_break(); coq_bol lexbuf end 
           else coq lexbuf
       }
@@ -556,7 +562,7 @@ and escaped_coq = parse
   | "["
       { incr brackets; Output.char '['; escaped_coq lexbuf }
   | "(*"
-      { ignore (comment lexbuf); escaped_coq lexbuf }
+      { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
   | "*)"
       { (* likely to be a syntax error: we escape *) backtrack lexbuf }
   | eof
@@ -591,16 +597,16 @@ and comments = parse
 (*s Skip comments *)
 
 and comment = parse
-  | "(*" { comment lexbuf }
-  | "*)" space* nl { true }
-  | "*)" { false }
-  | eof  { false }
-  | _    { comment lexbuf }
+  | "(*" { incr comment_level; comment lexbuf }
+  | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+  | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+  | eof  {  false }
+  | _    {  comment lexbuf }
 
 and skip_to_dot = parse
   | '.' space* nl { true }
   | eof | '.' space+ { false}
-  | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
+  | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
 and body_bol = parse
@@ -616,7 +622,8 @@ and body = parse
   | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
   | '.' space+ { Output.char '.'; Output.char ' '; false }
   | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
-  | "(*" { let eol = comment lexbuf in 
+  | "(*" { comment_level := 1; 
+	   let eol = comment lexbuf in 
 	     if eol 
 	     then begin Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }