diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-18 16:02:49 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-18 16:02:49 +0000 |
commit | f90854e62a8025eb1477c743dfef64a66f7da535 (patch) | |
tree | 4f3fb3a742e69c5c0212bb58cc18cb1ff609bc29 /tools/coqdoc | |
parent | 2da5db43c3937b7a74107d5a1e4e23a58ac6af28 (diff) |
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
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/cpretty.mll | 19 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 30 | ||||
-rw-r--r-- | tools/coqdoc/output.mli | 1 |
3 files changed, 39 insertions, 11 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 925f5258c..115bbe1cf 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 3aed28b45..fd192ca50 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 53d886668..b68857b27 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 |