Add --plain-comments patch by F. Garillot, which also adds

interpretation of [[ etc... inside (* *) comments when --parse-comments
is used. Add some additional fixes from B. Pierce on formatting
verbatim and the HTML Toc.


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

5 files changed, 85 insertions, 27 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index b3f0739d19..7e074802de 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -58,6 +58,7 @@ let coqlib = ref Coq_config.wwwstdlib
 let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
 let parse_comments = ref false
+let plain_comments = ref false
 let interpolate = ref false
 
 let charset = ref "iso-8859-1"
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 762be5aff6..b82caa7092 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -23,7 +23,6 @@ body { padding: 0px 0px;
 
 #main{ display: block;
        padding: 10px;
-       overflow: hidden;
        font-size: 100%;
        line-height: 100% }
 
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 5ca970f353..83639402fb 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -577,30 +577,40 @@ and doc = parse
   | nl
       { Output.char '\n'; doc_bol lexbuf }
   | "[[" nl
-      { formatted := true; Output.line_break (); Output.start_inline_coq ();
-	let eol = body_bol lexbuf in 
-	  Output.end_inline_coq (); formatted := false;
-	  if eol then doc_bol lexbuf else doc lexbuf}
+      { if !Cdglobals.plain_comments
+        then (Output.char '['; Output.char '['; doc lexbuf)
+        else (formatted := true; 
+              Output.line_break (); Output.start_inline_coq ();
+	      let eol = body_bol lexbuf in 
+	        Output.end_inline_coq (); formatted := false;
+	        if eol then doc_bol lexbuf else doc lexbuf)}
   | "["
-      { brackets := 1; 
-	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
-	doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '['
+        else (brackets := 1;  Output.start_inline_coq (); escaped_coq lexbuf;
+              Output.end_inline_coq ()); doc lexbuf }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
       { false }
   | "$"
-      { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '$'
+        else (Output.start_latex_math (); escaped_math_latex lexbuf);
+        doc lexbuf }
   | "$$"
-      { Output.char '$'; doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '$'; 
+        Output.char '$'; doc lexbuf }
   | "%"
-      { escaped_latex lexbuf; doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '%'
+        else escaped_latex lexbuf; doc lexbuf }
   | "%%"
-      { Output.char '%'; doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '%';
+        Output.char '%'; doc lexbuf }
   | "#"
-      { escaped_html lexbuf; doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '#'
+        else escaped_html lexbuf; doc lexbuf }
   | "##"
-      { Output.char '#'; doc lexbuf }
+      { if !Cdglobals.plain_comments then Output.char '#';
+        Output.char '#'; doc lexbuf }
   | eof 
       { false }
   | _ 
@@ -628,7 +638,7 @@ and escaped_html = parse
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
 and verbatim = parse
-  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
+  | nl ">>" space* nl? { Output.verbatim_char '\n'; Output.stop_verbatim () }
   | eof { Output.stop_verbatim () }
   | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
 
@@ -679,22 +689,64 @@ and comment = parse
 	   if !Cdglobals.parse_comments then Output.start_comment ();
 	   comment lexbuf }
   | "*)" space* nl {
-      if !Cdglobals.parse_comments then	(Output.end_comment (); Output.line_break ());
+      if !Cdglobals.parse_comments then	
+	(Output.end_comment (); Output.line_break ());
       decr comment_level; if !comment_level > 0 then comment lexbuf else true }
   | "*)" { 
       if !Cdglobals.parse_comments then (Output.end_comment ());
       decr comment_level; if !comment_level > 0 then comment lexbuf else false }
-  | "[" { 
-      if !Cdglobals.parse_comments then (
-	brackets := 1;
-	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
+  | "[" {
+      if !Cdglobals.parse_comments then
+	if !Cdglobals.plain_comments then Output.char '['
+        else (brackets := 1; Output.start_inline_coq ();
+              escaped_coq lexbuf; Output.end_inline_coq ());
       comment lexbuf }
+  | "[[" {
+      if !Cdglobals.parse_comments then
+        if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
+        else (formatted := true;
+              Output.line_break (); Output.start_inline_coq ();
+              let _ = body_bol lexbuf in
+                Output.end_inline_coq (); formatted := false);
+      comment lexbuf}
+  | "$"
+      { if !Cdglobals.parse_comments then
+          if !Cdglobals.plain_comments then Output.char '$'
+          else (Output.start_latex_math (); escaped_math_latex lexbuf);
+        comment lexbuf }
+  | "$$"
+      { if !Cdglobals.parse_comments 
+        then 
+          (if !Cdglobals.plain_comments then Output.char '$'; Output.char '$');
+        doc lexbuf }
+  | "%"
+      { if !Cdglobals.parse_comments
+          then 
+            if !Cdglobals.plain_comments then Output.char '%'
+            else escaped_latex lexbuf; comment lexbuf }
+  | "%%"
+      { if !Cdglobals.parse_comments 
+        then 
+          (if !Cdglobals.plain_comments then Output.char '%'; Output.char '%');
+        comment lexbuf }
+  | "#"
+      { if !Cdglobals.parse_comments
+        then
+          if !Cdglobals.plain_comments then Output.char '$'
+          else escaped_html lexbuf; comment lexbuf }
+  | "##"
+      { if !Cdglobals.parse_comments 
+        then 
+          (if !Cdglobals.plain_comments then Output.char '#'; Output.char '#');
+        comment lexbuf }
   | eof  { false }
-  | space+ { if !Cdglobals.parse_comments then 
-	Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
-  | nl   { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
+  | space+ { if !Cdglobals.parse_comments
+             then Output.indentation (fst (count_spaces (lexeme lexbuf)));
+             comment lexbuf }
+  | nl   { if !Cdglobals.parse_comments
+           then Output.line_break (); comment lexbuf }
   | _    { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
-  comment lexbuf }
+           comment lexbuf }
       
 and skip_to_dot = parse
   | '.' space* nl { true }
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index da65466ddf..301f4bdf70 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -66,6 +66,7 @@ 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 "";
   exit 1
 
@@ -276,6 +277,8 @@ 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
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 9fda0d0cad..b69e8b3695 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -668,14 +668,17 @@ module Html = struct
 	  printf "<hr/>"; print_table ()
 	end
 	    
-  let make_toc () = 
+	  
+  let make_toc () =
     let make_toc_entry = function
       | Toc_library m -> 
 	  stop_item ();
 	  printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m
       | Toc_section (n, f, r) ->
-	  item n; 
-	  printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+          if n <= 3 then begin
+	    item n; 
+	    printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+	  end
     in
       Queue.iter make_toc_entry toc_q;
       stop_item ();