coqdoc fixes and support for parsing regular comments (request by

B. Pierce on coq-club).
- Output regular comments, enclosed in a span in HTML (with (* *)
delimiters) and inside a new environment in LaTeX.
- HTML output: put the span inside anchors in links, so as to keep the
same style as for definitions (customizable in the CSS).
- Better handling of Next Obligation.


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

6 files changed, 119 insertions, 32 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5bcbed64e..c81dcec17 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -57,6 +57,7 @@ let externals = ref true
 let coqlib = ref "http://coq.inria.fr/library/"
 let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
+let parse_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 a9a997066..762be5aff 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -57,6 +57,11 @@ body { padding: 0px 0px;
     display: inline;
     font-family: monospace } 
 
+.comment { 
+    display: inline;
+    font-family: monospace;
+    color: red; } 
+
 .code { 
     display: block;
     font-family: monospace } 
@@ -80,18 +85,46 @@ body { padding: 0px 0px;
     color: rgb(40%,0%,40%);
 }
 
+.id[type="variable"] { 
+    color: rgb(40%,0%,40%);
+}
+
 .id[type="definition"] { 
     color: rgb(0%,40%,0%);
 }
 
+.id[type="abbreviation"] { 
+    color: rgb(0%,40%,0%);
+}
+
 .id[type="lemma"] { 
     color: rgb(0%,40%,0%);
 }
 
+.id[type="instance"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="projection"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="method"] { 
+    color: rgb(0%,40%,0%);
+}
+
 .id[type="inductive"] { 
     color: rgb(0%,0%,80%);
 }
 
+.id[type="record"] { 
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="class"] { 
+    color: rgb(0%,0%,80%);
+}
+
 .id[type="keyword"] { 
  color : #cf1d1d;
 /*     color: black; */
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 04f9ee4b0..24538360a 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -65,6 +65,7 @@ let usage () =
   prerr_endline "  --charset <string>   set HTML charset";
   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 "";
   exit 1
 
@@ -273,6 +274,8 @@ let parse () =
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
 	Cdglobals.raw_comments := true; parse_rec rem
+    | ("-parse-comments" | "--parse-comments") :: rem ->
+	Cdglobals.parse_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 568fade17..032c35caf 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -298,7 +298,7 @@ module Latex = struct
     else
       with_latex_printing (fun s -> ident s l) s
     
-  let symbol = with_latex_printing raw_ident
+  let symbol s = with_latex_printing raw_ident s
 
   let rec reach_item_level n = 
     if !item_level < n then begin
@@ -320,6 +320,12 @@ module Latex = struct
 
   let end_doc () = in_doc := false; stop_item ()
 
+  let comment c = char c
+
+  let start_comment () = printf "\\begin{coqdoccomment}\n"
+
+  let end_comment () = printf "\\end{coqdoccomment}\n"
+
   let start_coq () = printf "\\begin{coqdoccode}\n"
 
   let end_coq () = printf "\\end{coqdoccode}\n"
@@ -456,14 +462,15 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
 	printf "<span class=\"id\" type=\"%s\">" typ; 
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
-	printf "</a></span>"
+	raw_ident s;
+	printf "</span></a>"
     | Coqlib when !externals ->
 	let m = Filename.concat !coqlib m in
-	  printf "<span class=\"id\" type=\"%s\">" typ; 
 	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	  raw_ident s; printf "</a></span>"
+	  printf "<span class=\"id\" type=\"%s\">" typ; 
+	  raw_ident s; printf "</span></a>"
     | Coqlib | Unknown ->
 	printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
 	  
@@ -477,8 +484,9 @@ module Html = struct
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,ty) -> 
+		 printf "<a name=\"%s\">" fullid; 
 		 printf "<span class=\"id\" type=\"%s\">" (type_name ty); 
-		 printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
+		 raw_ident s; printf "</span></a>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
@@ -500,9 +508,11 @@ module Html = struct
     with Not_found -> 
       f tok
 
-  let ident s l = with_html_printing (fun s -> ident s l) s
+  let ident s l =
+    with_html_printing (fun s -> ident s l) s
 
-  let symbol = with_html_printing raw_ident
+  let symbol s =
+    with_html_printing raw_ident s
 
   let rec reach_item_level n = 
     if !item_level < n then begin
@@ -532,6 +542,10 @@ module Html = struct
     stop_item (); 
     if not !raw_comments then printf "\n</div>\n"
 
+  let start_comment () = printf "<span class=\"comment\">(*"
+
+  let end_comment () = printf "*)</span>"
+
   let start_code () = end_doc (); start_coq ()
 
   let end_code () = end_coq (); start_doc ()
@@ -770,6 +784,9 @@ module TeXmacs = struct
 
   let end_coq () = ()
 
+  let start_comment () = ()
+  let end_comment () = ()
+
   let start_code () = in_doc := true; printf "<\\code>\n"
   let end_code () = in_doc := false; printf "\n</code>"
 
@@ -849,7 +866,7 @@ module Raw = struct
 
   let ident s loc = raw_ident s
 
-  let symbol = raw_ident
+  let symbol s = raw_ident s
 
   let item n = printf "- "
 
@@ -858,6 +875,9 @@ module Raw = struct
   let start_doc () = printf "(** "
   let end_doc () = printf " *)\n"
 
+  let start_comment () = ()
+  let end_comment () = ()
+
   let start_coq () = ()
   let end_coq () = ()
 
@@ -911,6 +931,9 @@ let start_module =
 let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
 let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
 
+let start_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment
+let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment
+
 let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
 let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index f8fbb0fa4..181ccf1ca 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -28,6 +28,9 @@ val start_module : unit -> unit
 val start_doc : unit -> unit
 val end_doc : unit -> unit
 
+val start_comment : unit -> unit
+val end_comment : unit -> unit
+
 val start_coq : unit -> unit
 val end_coq : unit -> unit
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 1480624a5..c69ac0495 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -162,6 +162,8 @@
     else
       String.sub s 1 (String.length s - 3)
 
+  let symbol lexbuf s = Output.symbol s 
+
 }
 
 (*s Regular expressions *)
@@ -217,7 +219,10 @@ let thm_token =
   | "Proposition" 
   | "Property"
   | "Goal"
-  | "Next" space+ "Obligation"
+
+let prf_token =
+  "Next" space+ "Obligation"
+  | "Proof" (space* "." | space+ "with")
 
 let def_token = 
   "Definition" 
@@ -307,7 +312,6 @@ let prog_kw =
 
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
-  | "Next" "Obligation"
   | "Ltac"
   | "Require"
   | "Import"
@@ -343,7 +347,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -381,20 +385,20 @@ rule coq_bol = parse
 	  let eol = body lexbuf in
 	    in_proof := true;
 	    if eol then coq_bol lexbuf else coq lexbuf }
-  | space* "Proof" (space* "." | space+ "with")
+  | space* prf_token
       { in_proof := true;
 	let eol = 
 	if not !Cdglobals.gallina then 
 	  begin backtrack lexbuf; body_bol lexbuf end 
-	else true
+	else let s = lexeme lexbuf in
+	       if s.[String.length s - 1] = '.' then false
+	       else skip_to_dot lexbuf
 	in if eol then coq_bol lexbuf else coq lexbuf }
   | space* end_kw { 
       let eol = 
 	if not (!in_proof && !Cdglobals.gallina) then 
 	  begin backtrack lexbuf; body_bol lexbuf end 
-	else
-	  let eol = skip_to_dot lexbuf in
-	    if eol then Output.line_break (); eol
+	else skip_to_dot lexbuf
       in
 	in_proof := false;
 	if eol then coq_bol lexbuf else coq lexbuf }
@@ -442,6 +446,12 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { comment_level := 1; 
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
 	let eol = comment lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
@@ -467,12 +477,18 @@ and coq = parse
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { comment_level := 1;
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
 	let eol = comment lexbuf in
-	  if eol then begin Output.line_break(); coq_bol lexbuf end 
+	  if eol then coq_bol lexbuf
           else coq lexbuf
       }
   | nl+ space* "]]"
-      { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
   | gallina_kw_to_hide
@@ -492,9 +508,7 @@ and coq = parse
       let eol = 
 	if not (!in_proof && !Cdglobals.gallina) then 
 	  begin backtrack lexbuf; body lexbuf end 
-	else
-	  let eol = skip_to_dot lexbuf in
-	    if eol then Output.line_break (); eol
+	else skip_to_dot lexbuf
       in
 	in_proof := false;
 	if eol then coq_bol lexbuf else coq lexbuf }
@@ -617,8 +631,7 @@ and escaped_coq = parse
       { () }
   | token_brackets
       { let s = lexeme lexbuf in
-	Output.symbol s;
-	escaped_coq lexbuf }
+	  symbol lexbuf s; escaped_coq lexbuf }
   | (identifier '.')* identifier
       { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
   | _ 
@@ -646,11 +659,20 @@ and comments = parse
 
 and comment = parse
   | "(*" { 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 }
-
+  | "*)" space* nl { 
+      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 }
+  | 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 }
+  | _    { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+  comment lexbuf }
+      
 and skip_to_dot = parse
   | '.' space* nl { true }
   | eof | '.' space+ { false}
@@ -665,13 +687,15 @@ and body_bol = parse
 and body = parse
   | nl {Output.line_break(); body_bol lexbuf}
   | nl+ space* "]]"
-      { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
   | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
   | '.' space+ { Output.char '.'; Output.char ' '; false }
   | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
   | "(*" { comment_level := 1; 
+	   if !Cdglobals.parse_comments then Output.start_comment ();
 	   let eol = comment lexbuf in 
+	     if !Cdglobals.parse_comments then Output.end_comment ();
 	     if eol 
 	     then begin Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }
@@ -681,7 +705,7 @@ and body = parse
 	  body lexbuf }
   | token_no_brackets
       { let s = lexeme lexbuf in
-	  Output.symbol s; body lexbuf }
+	  symbol lexbuf s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           body lexbuf }
@@ -696,7 +720,7 @@ and notation = parse
   | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
-	  Output.symbol s; notation lexbuf }
+	  symbol lexbuf s; notation lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           notation lexbuf }