Various minor fixes to coqdoc from A. Chlipala.

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

4 files changed, 62 insertions, 16 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 925f5258ce..115bbe1cfb 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -254,7 +254,7 @@
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
     let s = String.sub s isp (String.length s - isp) in
-    Output.ident s (lexeme_start lexbuf + isp)
+    Output.keyword s (lexeme_start lexbuf + isp)
 
 }
 
@@ -369,13 +369,17 @@ let commands =
   | "Drop"
   | "ProtectedLoop"
   | "Quit"
+  | "Restart"
   | "Load"
   | "Add"
   | "Remove" space+ "Loadpath"
   | "Print"
   | "Inspect"
   | "About"
+  | "SearchAbout"
+  | "SearchRewrite"
   | "Search"
+  | "Locate"
   | "Eval"
   | "Reset"
   | "Check"
@@ -403,6 +407,14 @@ let prog_kw =
   | "Obligations"
   | "Solve"
 
+let hint_kw = 
+  "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
+
+let set_kw =
+    "Printing" space+ ("Coercions" | "Universes" | "All")
+  | "Implicit" space+ "Arguments"
+  
+
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
   | "Ltac"
@@ -410,15 +422,16 @@ let gallina_kw_to_hide =
   | "Import"
   | "Export"
   | "Load"
-  | "Hint"
+  | "Hint" space+ hint_kw
   | "Open"
   | "Close"
   | "Delimit"
   | "Transparent"
   | "Opaque"
   | ("Declare" space+ ("Morphism" | "Step") )
-  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | ("Set" | "Unset") space+ set_kw
   | "Declare" space+ ("Left" | "Right") space+ "Step"
+  | "Debug" space+ ("On" | "Off")
 
 
 let section = "*" | "**" | "***" | "****"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 3aed28b457..fd192ca50a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -31,7 +31,8 @@ let is_keyword =
   build_table
     [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
-      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar"; "Goal"; "Hint";
+      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+      "Guarded"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses";
       "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
@@ -53,6 +54,7 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      "fix"; "cofix";
       (* Ltac *)
       "before"; "after"
        ]
@@ -60,7 +62,10 @@ let is_keyword =
 let is_tactic =
   build_table
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-      "elimtype"; "progress"; "setoid_rewrite";
+      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
+      "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
       "set"; "assert"; "do"; "repeat";
@@ -69,7 +74,7 @@ let is_tactic =
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
       "pattern"; "intuition"; "congruence"; "fail"; "fresh";
-      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
+      "trivial"; "tauto"; "firstorder"; "ring";
       "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
 
 (*s Current Coq module *)
@@ -357,6 +362,9 @@ module Latex = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "\\coqdockw{%s}" (translate s)
+
   let ident s loc =
     try
       let tag = Index.find (get_module false) loc in
@@ -615,6 +623,9 @@ module Html = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+
   let ident s loc =
     if is_keyword s then begin
       printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
@@ -921,13 +932,14 @@ module TeXmacs = struct
 
   let indentation n = ()
 
+  let keyword s =
+    printf "<kw|"; raw_ident s; printf ">"
+
   let ident_true s =
-    if is_keyword s then begin
-      printf "<kw|"; raw_ident s; printf ">"
-    end else begin
-      raw_ident s
-    end
+    if is_keyword s then keyword s
+    else raw_ident s
 
+  let keyword s loc = keyword s
   let ident s _ = if !in_doc then ident_true s else raw_ident s
 
   let output_sublexer_string doescape issymbchar tag s =
@@ -1049,6 +1061,7 @@ module Raw = struct
   let indentation n =
       for i = 1 to n do printf " " done
 
+  let keyword s loc = raw_ident s
   let ident s loc = raw_ident s
 
   let sublexer c l = char c
@@ -1162,6 +1175,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
 let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
 let char = select Latex.char Html.char TeXmacs.char Raw.char
+let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
 let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 53d8866684..b68857b279 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -60,6 +60,7 @@ val rule : unit -> unit
 
 val nbsp : unit -> unit
 val char : char -> unit
+val keyword : string -> loc -> unit
 val ident : string -> loc -> unit
 val sublexer : char -> loc -> unit
 val initialize : unit -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1428503251..7942a6da26 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -420,6 +420,10 @@ let smart_global r =
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr;
     gr
 
+let dump_global r = 
+  let gr = Smartlocate.smart_global r in
+    Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
+
 (**********)
 (* Syntax *)
 
@@ -568,9 +572,21 @@ let vernac_cofixpoint l =
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_cofixpoint l
 
-let vernac_scheme = Indschemes.do_scheme
-
-let vernac_combined_scheme = Indschemes.do_combined_scheme
+let vernac_scheme l =
+  if Dumpglob.dump () then
+    List.iter (fun (lid, s) ->
+	       Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid;
+	       match s with
+	       | InductionScheme (_, r, _)
+	       | CaseScheme (_, r, _) 
+	       | EqualityScheme r -> dump_global r) l;
+  Indschemes.do_scheme l
+
+let vernac_combined_scheme lid l =
+  if Dumpglob.dump () then
+    (Dumpglob.dump_definition lid false "def";
+     List.iter (fun lid -> dump_global (AN (Ident lid))) l);
+ Indschemes.do_combined_scheme lid l
 
 (**********************)
 (* Modules            *)
@@ -1356,8 +1372,10 @@ let vernac_print = function
       msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
-  | PrintAbout qid -> msg_notice (print_about qid)
-  | PrintImplicit qid -> msg_notice (print_impargs qid)
+  | PrintAbout qid -> 
+    dump_global qid; msg_notice (print_about qid)
+  | PrintImplicit qid -> 
+    dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,r) ->
       (* Prints all the axioms and section variables used by a term *)
       let cstr = constr_of_global (smart_global r) in