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

7 files changed, 161 insertions, 72 deletions

diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 65c39b7a2..bb9d2886c 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -66,3 +66,29 @@ body { padding: 0px 0px;
 #footer a:link { text-decoration: none; 
                  color: #888888; }
 
+.id { display: inline; }
+
+.id[type="constructor"] { 
+    color: rgb(60%,0%,0%);
+}
+
+.id[type="var"] { 
+    color: rgb(40%,0%,40%);
+}
+
+.id[type="definition"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="lemma"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="inductive"] { 
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="keyword"] { 
+ color : #cf1d1d;
+/*     color: black; */
+}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 9831ca3cb..bfb57dad2 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -40,6 +40,8 @@ type index_entry =
 
 val find : coq_module -> loc -> index_entry
 
+val find_string : coq_module -> string -> index_entry
+
 val add_module : coq_module -> unit
 
 type module_kind = Local | Coqlib | Unknown
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 6a61571c6..5b5425590 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -47,9 +47,14 @@ let current_type = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-let table = Hashtbl.create 97
-  (** [table] is used to store references and definitions *)
+(** [deftable] stores only definitions and is used to interpolate idents 
+    inside comments, which are not globalized otherwise. *)
 
+let deftable = Hashtbl.create 97
+
+(** [reftable] stores references and definitions *)
+let reftable = Hashtbl.create 97
+  
 let full_ident sp id =
   if sp <> "<>" then 
     if id <> "<>" then 
@@ -60,15 +65,20 @@ let full_ident sp id =
   else ""
     
 let add_def loc ty sp id = 
-  Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
-
+  Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
+  Hashtbl.add deftable (!current_library, id) (Def (full_ident sp id, ty))
+    
 let add_ref m loc m' sp id ty = 
-  Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+  Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty))
     
-let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
-
-let find m l = Hashtbl.find table (m, l)
-
+let add_mod m loc m' id = 
+  Hashtbl.add reftable (m, loc) (Mod (m', id));
+  Hashtbl.add deftable (m, id) (Mod (m', id))
+    
+let find m l = Hashtbl.find reftable (m, l)
+  
+let find_string m s = Hashtbl.find deftable (m, s)
+  
 (*s Manipulating path prefixes *) 
 
 type stack = string list 
@@ -216,7 +226,7 @@ let all_entries () =
     | Def (s,t) -> add_g s m t; add_bt t s m
     | Ref _ | Mod _ -> ()
   in
-    Hashtbl.iter classify table;
+    Hashtbl.iter classify reftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global"; 
       idx_entries = sort_entries !gl; 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index d9384adc4..08707ba24 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -62,6 +62,7 @@ let usage () =
   prerr_endline "  --utf8               set UTF-8 input language";
   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 "";
   exit 1
 
@@ -267,6 +268,9 @@ let parse () =
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
 	Cdglobals.raw_comments := true; parse_rec rem
+    | ("-interpolate" | "--interpolate") :: rem ->
+	Cdglobals.interpolate := true; parse_rec rem
+
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
@@ -318,6 +322,7 @@ let parse () =
 	add_file (what_file f); parse_rec rem
   in 
     parse_rec (List.tl (Array.to_list Sys.argv));
+    Output.initialize ();
     List.rev !files
 
       
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index a5378e9df..a7ed7444a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -32,8 +32,8 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint";
-      "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
+    [ "AddPath"; "Axiom"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+      "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
       "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; 
@@ -42,7 +42,7 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Set"; "Unset"; "Variable"; "Variables"; "Context";
+      "Set"; "Types"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; 
       "Boxed"; "Unboxed"; "Inline";
@@ -53,8 +53,8 @@ let is_keyword =
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
       "Program Instance";
       (*i (* coq terms *) *)
-	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
-	"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
+      "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
+      "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
        ]
 
 let is_tactic = 
@@ -92,27 +92,29 @@ let find_printing_token tok =
 let remove_printing_token = Hashtbl.remove token_pp
 
 (* predefined pretty-prints *)
-let _ = List.iter 
-	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
-	  [ "*" ,  "\\ensuremath{\\times}";
-	    "|", "\\ensuremath{|}";
-	    "->",  "\\ensuremath{\\rightarrow}";
-	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
-	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
-	    "<-",  "\\ensuremath{\\leftarrow}";
-	    "<->", "\\ensuremath{\\leftrightarrow}";
-	    "=>",  "\\ensuremath{\\Rightarrow}";
-	    "<=",  "\\ensuremath{\\le}";
-	    ">=",  "\\ensuremath{\\ge}";
-	    "<>",  "\\ensuremath{\\not=}";
-	    "~",   "\\ensuremath{\\lnot}";
-	    "/\\", "\\ensuremath{\\land}";
-	    "\\/", "\\ensuremath{\\lor}";
-	    "|-",  "\\ensuremath{\\vdash}";
-	    "forall", "\\ensuremath{\\forall}";
-	    "exists", "\\ensuremath{\\exists}";
-	    (* "fun", "\\ensuremath{\\lambda}" ? *)
-	  ]
+let initialize () = 
+  let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
+    List.iter 
+      (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l'))
+      [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
+	"|", "\\ensuremath{|}", None;
+	"->",  "\\ensuremath{\\rightarrow}", if_utf8 "→";
+	"->~",  "\\ensuremath{\\rightarrow\\lnot}", None;
+	"->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}", None;
+	"<-",  "\\ensuremath{\\leftarrow}", None;
+	"<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔";
+	"=>",  "\\ensuremath{\\Rightarrow}", if_utf8 "⇒";
+	"<=",  "\\ensuremath{\\le}", if_utf8 "≤";
+	">=",  "\\ensuremath{\\ge}", if_utf8 "≥";
+	"<>",  "\\ensuremath{\\not=}", if_utf8 "≠";
+	"~",   "\\ensuremath{\\lnot}", if_utf8 "¬";
+	"/\\", "\\ensuremath{\\land}", if_utf8 "∧";
+	"\\/", "\\ensuremath{\\lor}", if_utf8 "∨";
+	"|-",  "\\ensuremath{\\vdash}", None;
+	"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
+	"exists", "\\ensuremath{\\exists}", if_utf8 "∃"
+	  (* "fun", "\\ensuremath{\\lambda}" ? *)
+      ]
 
 (*s Table of contents *)
 
@@ -243,30 +245,37 @@ module Latex = struct
 	  let _m = Filename.concat !coqlib m in
 	    printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib | Unknown ->
-	  raw_ident s
+	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
 
   let defref m id ty s =
     printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
 
+  let reference s = function
+    | Def (fullid,typ) -> 
+	defref !current_module fullid typ s
+    | Mod (m,s') when s = s' ->
+	module_ref m s
+    | Ref (m,fullid,typ) -> 
+	ident_ref m fullid typ s
+    | Mod _ ->
+	printf "\\coqdocid{"; raw_ident s; printf "}"
+
   let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
     end else begin
       begin
 	try
-	  (match Index.find !current_module loc with
-	     | Def (fullid,typ) -> 
-		 defref !current_module fullid typ s
-             | Mod (m,s') when s = s' ->
-		 module_ref m s
-	     | Ref (m,fullid,typ) -> 
-		 ident_ref m fullid typ s
-	     | Mod _ ->
-		 printf "\\coqdocid{"; raw_ident s; printf "}")
+	  reference s (Index.find !current_module loc)
 	with Not_found ->
 	  if is_tactic s then begin
 	    printf "\\coqdoctac{"; raw_ident s; printf "}"
-	  end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
+	  end else begin
+	    if !Cdglobals.interpolate then
+	      try reference s (Index.find_string !current_module s)
+	      with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" 
+	    else printf "\\coqdocvar{"; raw_ident s; printf "}"
+	  end
       end
     end
 
@@ -394,7 +403,8 @@ module Html = struct
 
   let line_break () = printf "<br/>\n"
 
-  let empty_line_of_code () = printf "\n<br/>\n"
+  let empty_line_of_code () = 
+    printf "\n<br/>\n"
 
   let char = function
     | '<' -> printf "&lt;"
@@ -426,37 +436,43 @@ module Html = struct
       | Coqlib | Unknown ->
 	  raw_ident s
 
-  let ident_ref m fid s = 
+  let ident_ref m fid typ s =
     match find_module m with
-      | Local ->
-	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
-      | Coqlib when !externals ->
-	  let m = Filename.concat !coqlib m in
-	    printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
-      | Coqlib | Unknown ->
-	  raw_ident s
-
+    | Local ->
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; 
+	printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div></a>"
+    | Coqlib when !externals ->
+	let m = Filename.concat !coqlib m in
+	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
+	  printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div></a>"
+    | Coqlib | Unknown ->
+	printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div>"
+	  
   let ident s loc = 
     if is_keyword s then begin
-      printf "<span class=\"keyword\">"; 
+      printf "<div class=\"id\" type=\"keyword\">"; 
       raw_ident s; 
-      printf "</span>"
+      printf "</div>"
     end else 
       begin
 	try
 	  (match Index.find !current_module loc with
-	     | Def (fullid,_) -> 
-		 printf "<a name=\"%s\"></a>" fullid; raw_ident s
+	     | Def (fullid,ty) -> 
+		 printf "<a name=\"%s\">" fullid; 
+		 printf "<div class=\"id\" type=\"%s\">" (type_name ty); raw_ident s; printf "</div></a>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
-		 ident_ref m fullid s
+		 ident_ref m fullid (type_name ty) s
 	     | Mod _ ->
-		 raw_ident s)
+		 printf "<div class=\"id\" type=\"mod\">"; raw_ident s ; printf "</div>")
 	with Not_found ->
-	  raw_ident s
+	  if is_tactic s then
+	    (printf "<div class=\"id\" type=\"tactic\">"; raw_ident s; printf "</div>")
+	  else
+	    (printf "<div class=\"id\" type=\"var\">"; raw_ident s ; printf "</div>")
       end
-	  
+
   let with_html_printing f tok =
     try 
       (match Hashtbl.find token_pp tok with
@@ -536,7 +552,7 @@ module Html = struct
   let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
 
   (* Construction d'une liste des index (1 index global, puis 1
-     index par catégorie) *)
+     index par catégorie) *)
   let format_global_index =
     Index.map 
       (fun s (m,t) -> 
@@ -575,7 +591,7 @@ module Html = struct
     printf "</table>\n"
 	
   let make_one_multi_index prt_tbl i =
-    (* Attn: make_one_multi_index créé un nouveau fichier... *)
+    (* Attn: make_one_multi_index créé un nouveau fichier... *)
     let idx = i.idx_name in
     let one_letter ((c,l) as cl) =
       open_out_file (sprintf "index_%s_%c.html" idx c);
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 824e267e5..f8fbb0fa4 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -11,6 +11,8 @@
 open Cdglobals
 open Index
 
+val initialize : unit -> unit
+
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
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