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

1 files changed, 32 insertions, 9 deletions

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