Correction du bug #1512

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

2 files changed, 47 insertions, 29 deletions

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index c3a32f08ff..a4653d9b7a 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -421,28 +421,33 @@ 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 = function
+  | Vernac_file (f,m) ->   
+      let glob = (Filename.chop_extension f) ^ ".glob" in
+	(try
+	  Index.read_glob glob
+	with 
+	    _ -> eprintf "Warning: file %s cannot be opened; links will not be available\n" glob)
+  | Latex_file _ -> ()
 
-let glob_filename f =
-  (Filename.chop_extension f) ^ ".glob"
-    
 let index_module = function
   | Vernac_file (f,m) ->   
-      Index.read_glob (glob_filename f);
       Index.add_module m
   | Latex_file _ -> ()
       
 let produce_document l =
-  List.iter index_module 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
-      copy src dst);
+      copy src dst;
+      List.iter read_glob l);
   (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
       copy src dst);
+  List.iter index_module l;
   match !out_to with
     | StdOut -> 
 	Cdglobals.out_channel := stdout;
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 686197f9b8..1a2c5d866d 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -168,6 +168,7 @@
 
 let space = [' ' '\t']
 let space_nl = [' ' '\t' '\n' '\r']
+let nl = "\r\n" | '\n'
 
 let firstchar = 
   ['A'-'Z' 'a'-'z' '_' 
@@ -312,10 +313,10 @@ let section = "*" | "**" | "***" | "****"
 
 let item_space = "    "
 
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* '\n'
-let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* '\n'
-let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* '\n'
-let end_show = "(*" space* "end" space+ "show" space* "*)" space* '\n'
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
+let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
+let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
+let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
 (*
 let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
@@ -326,7 +327,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 (*s Scanning Coq, at beginning of line *)
 
 rule coq_bol = parse
-  | space* '\n'+
+  | space* nl+
       { empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { end_coq (); start_doc (); 
@@ -345,10 +346,8 @@ rule coq_bol = parse
   | space* gallina_kw_to_hide
       { let s = lexeme lexbuf in
 	  if !light && section_or_end s then 
-	    begin 
-	      skip_to_dot lexbuf; 
-	      coq_bol lexbuf 
-	    end 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then (line_break (); coq_bol lexbuf) else coq lexbuf
 	  else 
 	    begin
 	      let nbsp = count_spaces s in
@@ -413,7 +412,7 @@ rule coq_bol = parse
 (*s Scanning Coq elsewhere *)
 
 and coq = parse
-  | "\n" 
+  | nl 
       { line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { end_coq (); start_doc (); 
@@ -425,7 +424,7 @@ and coq = parse
 	  if eol then begin line_break(); coq_bol lexbuf end 
           else coq lexbuf
       }
-  | '\n'+ space* "]]"
+  | nl+ space* "]]"
       { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
@@ -455,18 +454,19 @@ and coq = parse
   | space+ { char ' '; coq lexbuf }
   | eof 
       { () }
-  | _ { let eol = 
+  | _ {	let eol = 
 	  if not !gallina then 
 	    begin backtrack lexbuf; indentation 0; body lexbuf end 
 	  else 
-	    skip_to_dot lexbuf 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then line_break (); eol
 	in 
 	  if eol then coq_bol lexbuf else coq lexbuf}
       
 (*s Scanning documentation, at beginning of line *)
 
 and doc_bol = parse
-  | space* "\n" '\n'*
+  | space* nl+
       { paragraph (); doc_bol lexbuf }
   | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
       { let eol, lex = strip_eol (lexeme lexbuf) in
@@ -487,19 +487,19 @@ and doc_bol = parse
 (*s Scanning documentation elsewhere *)
 
 and doc = parse
-  | "\n"
+  | nl
       { char '\n'; doc_bol lexbuf }
   | "["
       { brackets := 1; 
 	start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
 	doc lexbuf }
-  | "[[" '\n' space*
+  | "[[" nl space*
       { formatted := true; line_break (); start_inline_coq ();
 	indentation (count_spaces (lexeme lexbuf)); 
 	let eol = body_bol lexbuf in 
 	  end_inline_coq (); formatted := false;
 	  if eol then doc_bol lexbuf else doc lexbuf}
-  | '*'* "*)" space* '\n'
+  | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
       { false }
@@ -542,7 +542,7 @@ and escaped_html = parse
   | _   { html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
 and verbatim = parse
-  | "\n>>" { verbatim_char '\n'; stop_verbatim () }
+  | "nl>>" { verbatim_char '\n'; stop_verbatim () }
   | eof { stop_verbatim () }
   | _ { verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
 
@@ -591,13 +591,13 @@ and comments = parse
 
 and comment = parse
   | "(*" { comment lexbuf }
-  | "*)" space* '\n'+ { true }
+  | "*)" space* nl+ { true }
   | "*)" { false }
   | eof  { false }
   | _    { comment lexbuf }
 
 and skip_to_dot = parse
-  | '.' space* '\n' { true }
+  | '.' space* nl { true }
   | eof | '.' space+ { false}
   | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
@@ -608,12 +608,13 @@ and body_bol = parse
   | _ { backtrack lexbuf; body lexbuf }
 
 and body = parse
-  | '\n' {line_break(); body_bol lexbuf}
-  | '\n'+ space* "]]"
+  | nl {line_break(); body_bol lexbuf}
+  | nl+ space* "]]"
       { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
-  | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
+  | '.' space* nl | '.' space* eof { char '.'; line_break(); true }      
   | '.' space+ { char '.'; char ' '; false }
+  | '"' { char '"'; notation lexbuf; body lexbuf }
   | "(*" { let eol = comment lexbuf in 
 	     if eol 
 	     then begin line_break(); body_bol lexbuf end
@@ -629,6 +630,18 @@ and body = parse
 	  char c; 
           body lexbuf }
 
+and notation_bol = parse
+  | space+
+      { indentation (count_spaces (lexeme lexbuf)); notation lexbuf }
+  | _ { backtrack lexbuf; notation lexbuf }
+
+and notation = parse
+  | nl { line_break(); notation_bol lexbuf }
+  | '"' { char '"'; false }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  char c; 
+          notation lexbuf }
+
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }