summaryrefslogtreecommitdiff
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml151
1 files changed, 119 insertions, 32 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 3aed28b4..cd33528a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -31,21 +31,25 @@ 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"; "Debug"; "On";
"Hypothesis"; "Hypotheses";
- "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+ "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
+ "Implicit"; "Import"; "Inductive";
"Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
"Module"; "Module Type"; "Declare Module"; "Include";
- "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "Proof"; "Proof with"; "Qed";
- "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+ "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
+ "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
"Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+ "Search"; "SearchAbout"; "SearchRewrite";
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
"Delimit"; "Bind"; "Open"; "Scope"; "Inline";
"Implicit Arguments"; "Add"; "Strict";
"Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
- "subgoal"; "vm_compute";
- "Opaque"; "Transparent";
+ "subgoal"; "subgoals"; "vm_compute";
+ "Opaque"; "Transparent"; "Time";
+ "Extraction"; "Extract";
(* Program *)
"Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -53,14 +57,20 @@ 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"
+ "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+ (* Notations *)
+ "level"; "associativity"; "no"
]
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,8 +79,10 @@ let is_tactic =
"reflexivity"; "symmetry"; "transitivity";
"replace"; "setoid_replace"; "inversion"; "inversion_clear";
"pattern"; "intuition"; "congruence"; "fail"; "fresh";
- "trivial"; "exact"; "tauto"; "firstorder"; "ring";
- "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
+ "trivial"; "tauto"; "firstorder"; "ring";
+ "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto";
+ "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose";
+ "eval"; "instantiate"; "until" ]
(*s Current Coq module *)
@@ -261,6 +273,12 @@ module Latex = struct
| '^' | '~' as c ->
Buffer.add_char buff '\\'; Buffer.add_char buff c;
Buffer.add_string buff "{}"
+ | '\'' ->
+ if i < String.length s - 1 && s.[i+1] = '\'' then begin
+ Buffer.add_char buff '\''; Buffer.add_char buff '{';
+ Buffer.add_char buff '}'
+ end else
+ Buffer.add_char buff '\''
| c ->
Buffer.add_char buff c
done;
@@ -282,9 +300,23 @@ module Latex = struct
let stop_latex_math () = output_char '$'
- let start_verbatim () = printf "\\begin{verbatim}"
+ let start_quote () = output_char '`'; output_char '`'
+ let stop_quote () = output_char '\''; output_char '\''
+
+ let start_verbatim inline =
+ if inline then printf "\\texttt{"
+ else printf "\\begin{verbatim}"
- let stop_verbatim () = printf "\\end{verbatim}\n"
+ let stop_verbatim inline =
+ if inline then printf "}"
+ else printf "\\end{verbatim}\n"
+
+ let url addr name =
+ printf "%s\\footnote{\\url{%s}}"
+ (match name with
+ | None -> ""
+ | Some n -> n)
+ addr
let indentation n =
if n == 0 then
@@ -342,11 +374,19 @@ module Latex = struct
| Some ref -> reference s ref
| None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
+ let last_was_in = ref false
+
let sublexer c loc =
- let tag =
- try Some (Index.find (get_module false) loc) with Not_found -> None
- in
- Tokens.output_tagged_symbol_char tag c
+ if c = '*' && !last_was_in then begin
+ Tokens.flush_sublexer ();
+ output_char '*'
+ end else begin
+ let tag =
+ try Some (Index.find (get_module false) loc) with Not_found -> None
+ in
+ Tokens.output_tagged_symbol_char tag c
+ end;
+ last_was_in := false
let initialize () =
Tokens.token_tree := token_tree_latex;
@@ -357,7 +397,11 @@ 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 =
+ last_was_in := s = "in";
try
let tag = Index.find (get_module false) loc in
reference (translate s) tag
@@ -559,8 +603,22 @@ module Html = struct
let start_latex_math () = ()
let stop_latex_math () = ()
- let start_verbatim () = printf "<pre>"
- let stop_verbatim () = printf "</pre>\n"
+ let start_quote () = char '"'
+ let stop_quote () = start_quote ()
+
+ let start_verbatim inline =
+ if inline then printf "<tt>"
+ else printf "<pre>"
+
+ let stop_verbatim inline =
+ if inline then printf "</tt>"
+ else printf "</pre>\n"
+
+ let url addr name =
+ printf "<a href=\"%s\">%s</a>" addr
+ (match name with
+ | Some n -> n
+ | None -> addr)
let module_ref m s =
match find_module m with
@@ -615,6 +673,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)
@@ -915,19 +976,28 @@ module TeXmacs = struct
let stop_latex_math () = output_char '>'
- let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+ let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+ let stop_verbatim inline = in_doc := false; printf "</verbatim>"
- let stop_verbatim () = in_doc := false; printf "</verbatim>"
+ let url addr name =
+ printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+ (match name with
+ | None -> ""
+ | Some n -> n)
+
+ let start_quote () = output_char '`'; output_char '`'
+ let stop_quote () = output_char '\''; output_char '\''
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 =
@@ -1042,13 +1112,21 @@ module Raw = struct
let start_latex_math () = ()
let stop_latex_math () = ()
- let start_verbatim () = ()
+ let start_verbatim inline = ()
+ let stop_verbatim inline = ()
+
+ let url addr name =
+ match name with
+ | Some n -> printf "%s (%s)" n addr
+ | None -> printf "%s" addr
- let stop_verbatim () = ()
+ let start_quote () = printf "\""
+ let stop_quote () = printf "\""
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 +1240,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
@@ -1189,12 +1268,20 @@ let start_verbatim =
select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
let stop_verbatim =
select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
- select output_char Html.char TeXmacs.char Raw.char
+let verbatim_char inline =
+ select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
let hard_verbatim_char = output_char
+let url =
+ select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+ select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+ select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
- start_verbatim ();
+ start_verbatim false;
let dumb_line =
function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
char '\n')
@@ -1204,7 +1291,7 @@ let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
| Some s -> " " ^ s
| None -> ""));
List.iter dumb_line conclusions);
- stop_verbatim ()
+ stop_verbatim false
let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb