r8636@thot: notin | 2006-03-14 15:57:11 +0100

 Correction de bugs de Coqdoc


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

2 files changed, 16 insertions, 13 deletions

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index d43df8d34..865f101f6 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -75,10 +75,9 @@ let banner () =
   flush stderr
 
 let target_full_name f = 
-  let basefile = chop_suffix f ".v" in
-    match !target_language with
-      | HTML -> basefile ^ ".html"
-      | _ -> basefile ^ ".tex"
+  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
@@ -384,12 +383,12 @@ let gen_mult_files l =
   let file = function
     | Vernac_file (f,m) -> 
 	set_module m;
-	let hf = target_full_name f in
+	let hf = target_full_name m in
 	  open_out_file hf;
-	  header (); 
+	  if (!header_trailer) then header (); 
 	  if !toc then make_toc ();
 	  coq_file f m; 
-	  trailer ();
+	  if (!header_trailer) then trailer ();
 	  close_out_file()
     | Latex_file _ -> ()
   in
@@ -397,16 +396,18 @@ let gen_mult_files l =
     if (!index && !target_language=HTML) then begin
       open_out_file "index.html"; 
       page_title := (if !title <> "" then !title else "Index");
-      header (); make_index (); trailer ();
+      if (!header_trailer) then header (); 
+      make_index (); 
+      if (!header_trailer) then trailer ();
       close_out_file()
     end;
     if (!toc && !target_language=HTML) then begin
       open_out_file "toc.html"; 
       page_title := (if !title <> "" then !title else "Table of contents");
-      header ();
+      if (!header_trailer) then header ();
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
       make_toc (); 
-      trailer ();
+      if (!header_trailer) then trailer ();
       close_out_file()
     end 
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 9d695950c..2acb41407 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -303,7 +303,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 (*s Scanning Coq, at beginning of line *)
 
 rule coq_bol = parse
-  | '\n'+
+  | space* '\n'+
       { empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { end_coq (); start_doc (); 
@@ -404,9 +404,11 @@ and coq = parse
 	  let eol = body lexbuf in
 	    if eol then coq_bol lexbuf else coq lexbuf }
   | space+ { char ' '; coq lexbuf }
+  |  eof 
+      { () }
   | _ { let eol = 
 	  if not !gallina then 
-	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	    begin backtrack lexbuf; indentation 0; body lexbuf end 
 	  else 
 	    skip_to_dot lexbuf 
 	in 
@@ -558,7 +560,7 @@ and body_bol = parse
 and body = parse
   | '\n' {line_break(); body_bol lexbuf}
   | eof { false }
-  | '.' space* '\n' { char '.'; line_break(); true }      
+  | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
   | '.' space+ { char '.'; char ' '; false }
   | "(*" { let eol = comment lexbuf in 
 	     if eol then body_bol lexbuf else body lexbuf }