Preserve ordinary comments within proof scripts.

doc/coq2html.css

@@ -7,6 +7,7 @@
      div.proofscript  contents of proof script
      span.docright contents of (**r *) comments
      span.bracket contents of [ ] within comments
+     span.comment contents of (* *) comments
      span.kwd     Coq keyword
      span.tactic  Coq tactic
      span.id      any other identifier
@@ -86,6 +87,10 @@ span.kwd {
   color:  #cf1d1d;
 }
 
+span.comment {
+  color:  #008000;
+}
+
 a:visited {color : #416DFF; text-decoration : none; }
 a:link {color : #416DFF; text-decoration : none; }
 a:hover {text-decoration : none; }

doc/coq2html.mll

@@ -206,23 +206,32 @@ let start_verbatim () =
 let end_verbatim () =
   fprintf !oc "</pre>\n"
 
+let start_comment () =
+  fprintf !oc "<span class=\"comment\">(*"
+
+let end_comment () =
+  fprintf !oc "*)</span>"
+
 let start_bracket () =
   fprintf !oc "<span class=\"bracket\">"
 
 let end_bracket () =
   fprintf !oc "</span>"
 
+let in_proof = ref false
 let proof_counter = ref 0
 
 let start_proof kwd =
+  in_proof := true;
   incr proof_counter;
   fprintf !oc
   "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n"
     !proof_counter kwd;
   fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter
 
 let end_proof kwd =
-  fprintf !oc "%s</div>\n" kwd
+  fprintf !oc "%s</div>\n" kwd;
+  in_proof := false
 
 let start_html_page modname =
   fprintf !oc "\
@@ -300,7 +309,8 @@ and coq = parse
         end_doc_right();
         coq lexbuf }
   | "(*"
-      { comment lexbuf;
+      { if !in_proof then start_comment();
+        comment lexbuf;
         coq lexbuf }
   | path as id
       { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf }
@@ -325,13 +335,23 @@ and bracket = parse
 
 and comment = parse
   | "*)"
-      { () }
+      { if !in_proof then end_comment() }
   | "(*"
-      { comment lexbuf; comment lexbuf }
+      { if !in_proof then start_comment(); 
+        comment lexbuf; comment lexbuf }
   | eof
       { () }
-  | _
-      { comment lexbuf }
+  | "\n"
+      { if !in_proof then newline();
+        comment lexbuf }
+  | space* as s
+      { if !in_proof then space s; 
+        comment lexbuf }
+  | eof
+      { () }
+  | _ as c
+      { if !in_proof then character c;
+        comment lexbuf }
 
 and doc_bol = parse
   | "<<" space* "\n"