Improvements in coqdoc:

- Better handling of spaces by actually ignoring what's inside proof
scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs
[Proof t.] and [Qed]/[Save]/...).
- Provide fancy replacements for forall,/\,... etc in HTML in case the 
utf8 option is on.
- Use typesetting information in HTML output and customize the CSS
accordingly. The default color scheme follows closely the one set by
Conor for Epigram; of course one can change it.
- A try at interpolating identifiers in comments if they are defined in
the same module, with a corresponding flag.


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

1 files changed, 33 insertions, 5 deletions

diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index b02133285..fc40a97c5 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -57,6 +57,7 @@
   let formatted = ref false
   let brackets = ref 0
   let comment_level = ref 0
+  let in_proof = ref false
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -214,7 +215,7 @@ let def_token =
   "Definition" 
   | "Let" 
   | "Class"
-  | "SubClass" 
+  | "SubClass"
   | "Example"
   | "Local" 
   | "Fixpoint" 
@@ -278,6 +279,8 @@ let commands =
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
+let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted"
+
 let extraction = 
   "Extraction"
   | "Recursive" space+ "Extraction" 
@@ -292,7 +295,7 @@ let prog_kw =
   | "Solve"
 
 let gallina_kw_to_hide =
-  "Implicit"
+    "Implicit" space+ "Arguments"
   | "Ltac"
   | "Require"
   | "Import"
@@ -304,6 +307,7 @@ let gallina_kw_to_hide =
   | "Delimit"
   | "Transparent"
   | "Opaque"
+  | "Proof" space+ "with"
   | ("Declare" space+ ("Morphism" | "Step") )
   | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
   | "Declare" space+ ("Left" | "Right") space+ "Step" 
@@ -334,7 +338,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -353,7 +357,7 @@ rule coq_bol = parse
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then 
 	    let eol = skip_to_dot lexbuf in
-	      if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf
+	      if eol then (coq_bol lexbuf) else coq lexbuf
 	  else 
 	    begin
 	      let nbsp,isp = count_spaces s in
@@ -363,6 +367,30 @@ rule coq_bol = parse
 		  let eol = body lexbuf in 
 		    if eol then coq_bol lexbuf else coq lexbuf
 	    end }
+  | space* thm_token
+      { let s = lexeme lexbuf in 
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
+	  Output.indentation nbsp;
+	  Output.ident s (lexeme_start lexbuf + isp); 
+	  let eol = body lexbuf in
+	    in_proof := true;
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space* "Proof" (space* "." | space+ "with")
+      { let eol = 
+	if not !Cdglobals.gallina then 
+	  begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end 
+	else true
+	in if eol then coq_bol lexbuf else coq lexbuf }
+  | space* end_kw { 
+      in_proof := false;
+      let eol = 
+	if not !Cdglobals.gallina then 
+	  begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end 
+	else
+	  skip_to_dot lexbuf 
+      in
+	if eol then coq_bol lexbuf else coq lexbuf }
   | space* gallina_kw
       { let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
@@ -420,7 +448,7 @@ rule coq_bol = parse
 
 and coq = parse
   | nl 
-      { Output.line_break(); coq_bol lexbuf }
+      { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in