diff options
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 365 |
1 files changed, 242 insertions, 123 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 93414f22..c146150c 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*) +(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*) open Cdglobals open Index @@ -32,43 +32,48 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "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"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; - "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; + "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Set"; "Unset"; "Variable"; "Variables"; "Context"; + "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; - "Arguments"; "Add"; "Strict"; - "Typeclasses"; "Instance"; "Class"; "Instantiation"; + "Implicit Arguments"; "Add"; "Strict"; + "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; + "subgoal"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; - "Program Instance"; + "Program Instance"; "Equations"; "Equations_nocomp"; (*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"; "struct"; "wf"; "measure"; + (* Ltac *) + "before"; "after" ] let is_tactic = build_table - [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite"; - "destruct"; "induction"; "elim"; "dependent"; - "generalize"; "clear"; "rename"; "move"; "set"; "assert"; - "cut"; "assumption"; "exact"; "split"; "try"; "discriminate"; + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; + "set"; "assert"; "do"; "repeat"; + "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; "transitivity"; "replace"; "setoid_replace"; "inversion"; "inversion_clear"; - "pattern"; "intuition"; "congruence"; + "pattern"; "intuition"; "congruence"; "fail"; "fresh"; "trivial"; "exact"; "tauto"; "firstorder"; "ring"; - "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ] + "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ] (*s Current Coq module *) @@ -92,27 +97,31 @@ 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 "∃"; + "Î ", "\\ensuremath{\\Pi}", if_utf8 "Î "; + "λ", "\\ensuremath{\\lambda}", if_utf8 "λ" + (* "fun", "\\ensuremath{\\lambda}" ? *) + ] (*s Table of contents *) @@ -130,6 +139,9 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r module Latex = struct + let in_title = ref false + let in_doc = ref false + (*s Latex preamble *) let (preamble : string Queue.t) = Queue.create () @@ -208,7 +220,7 @@ module Latex = struct let indentation n = if n == 0 then - printf "\\noindent\n" + printf "\\coqdocnoindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space @@ -243,35 +255,49 @@ 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 "\\coqdocvar{"; 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 && !in_doc (* always a var otherwise *) + 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 - let ident s l = with_latex_printing (fun s -> ident s l) s - + let ident s l = + if !in_title then ( + printf "\\texorpdfstring{"; + with_latex_printing (fun s -> ident s l) s; + printf "}{"; raw_ident s; printf "}") + else + with_latex_printing (fun s -> ident s l) s + let symbol = with_latex_printing raw_ident let rec reach_item_level n = @@ -290,13 +316,13 @@ module Latex = struct let stop_item () = reach_item_level 0 - let start_doc () = printf "\n\n\n\\noindent\n" + let start_doc () = in_doc := true - let end_doc () = stop_item (); printf "\n\n\n" + let end_doc () = in_doc := false; stop_item () - let start_coq () = () + let start_coq () = printf "\\begin{coqdoccode}\n" - let end_coq () = () + let end_coq () = printf "\\end{coqdoccode}\n" let start_code () = end_doc (); start_coq () @@ -312,17 +338,17 @@ module Latex = struct let section lev f = stop_item (); output_string (section_kind lev); - f (); + in_title := true; f (); in_title := false; printf "}\n\n" let rule () = printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" - let paragraph () = stop_item (); printf "\n\n\\medskip\n" + let paragraph () = stop_item (); printf "\n\n" let line_break () = printf "\\coqdoceol\n" - let empty_line_of_code () = printf "\n\n\\medskip\n" + let empty_line_of_code () = printf "\\coqdocemptyline\n" let start_inline_coq () = () @@ -394,7 +420,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 "<" @@ -417,49 +444,54 @@ module Html = struct let stop_verbatim () = printf "</pre>\n" let module_ref m s = - printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" - (*i - match find_module m with - | Local -> - printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" - | Coqlib | Unknown -> - raw_ident s - i*) - - let ident_ref m fid s = match find_module m with | Local -> - printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>" + printf "<a class=\"modref\" href=\"%s.html\">" m; 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>" + printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" | Coqlib | Unknown -> raw_ident s + let ident_ref m fid typ s = + match find_module m with + | Local -> + printf "<span class=\"id\" type=\"%s\">" typ; + printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; + printf "</a></span>" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "<span class=\"id\" type=\"%s\">" typ; + printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; + raw_ident s; printf "</a></span>" + | Coqlib | Unknown -> + printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>" + let ident s loc = if is_keyword s then begin - printf "<span class=\"keyword\">"; + printf "<span class=\"id\" type=\"keyword\">"; raw_ident s; printf "</span>" 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 "<span class=\"id\" type=\"%s\">" (type_name ty); + printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>" | 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 "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>") with Not_found -> - raw_ident s + if is_tactic s then + (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>") + else + (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>") end - + let with_html_printing f tok = try (match Hashtbl.find token_pp tok with @@ -488,9 +520,9 @@ module Html = struct let stop_item () = reach_item_level 0 - let start_coq () = if not !raw_comments then printf "<code>\n" + let start_coq () = if not !raw_comments then printf "<div class=\"code\">\n" - let end_coq () = if not !raw_comments then printf "</code>\n" + let end_coq () = if not !raw_comments then printf "</div>\n" let start_doc () = if not !raw_comments then @@ -504,9 +536,9 @@ module Html = struct let end_code () = end_coq (); start_doc () - let start_inline_coq () = printf "<code>" + let start_inline_coq () = printf "<span class=\"inlinecode\">" - let end_inline_coq () = printf "</code>" + let end_inline_coq () = printf "</span>" let paragraph () = stop_item (); printf "\n<br/><br/>\n" @@ -539,7 +571,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) -> @@ -578,7 +610,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); @@ -776,68 +808,155 @@ module TeXmacs = struct end + +(*s LaTeX output *) + +module Raw = struct + + let header () = () + + let trailer () = () + + let char = output_char + + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + + let latex_char = output_char + let latex_string = output_string + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = () + let end_module () = () + + let start_latex_math () = () + let stop_latex_math () = () + + let start_verbatim () = () + + let stop_verbatim () = () + + let indentation n = + for i = 1 to n do printf " " done + + let ident s loc = raw_ident s + + let symbol = raw_ident + + let item n = printf "- " + + let stop_item () = () + + let start_doc () = printf "(** " + let end_doc () = printf " *)\n" + + let start_coq () = () + let end_coq () = () + + let start_code () = end_doc (); start_coq () + let end_code () = end_coq (); start_doc () + + let section_kind = + function + | 1 -> "*" + | 2 -> "**" + | 3 -> "***" + | 4 -> "****" + | _ -> assert false + + let section lev f = + output_string (section_kind lev); + f () + + let rule () = () + + let paragraph () = printf "\n\n" + + let line_break () = printf "\n" + + let empty_line_of_code () = printf "\n" + + let start_inline_coq () = () + let end_inline_coq () = () + + let make_multi_index () = () + let make_index () = () + let make_toc () = () + +end + + + (*s Generic output *) -let select f1 f2 f3 x = - match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x +let select f1 f2 f3 f4 x = + match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x let push_in_preamble = Latex.push_in_preamble -let header = select Latex.header Html.header TeXmacs.header -let trailer = select Latex.trailer Html.trailer TeXmacs.trailer +let header = select Latex.header Html.header TeXmacs.header Raw.header +let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer let start_module = - select Latex.start_module Html.start_module TeXmacs.start_module + select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module -let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc -let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc +let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc +let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc -let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq -let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq +let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq +let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq -let start_code = select Latex.start_code Html.start_code TeXmacs.start_code -let end_code = select Latex.end_code Html.end_code TeXmacs.end_code +let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code let start_inline_coq = - select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq + select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = - select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq + select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq -let indentation = select Latex.indentation Html.indentation TeXmacs.indentation -let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph -let line_break = select Latex.line_break Html.line_break TeXmacs.line_break +let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation +let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph +let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break let empty_line_of_code = select - Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code + Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code -let section = select Latex.section Html.section TeXmacs.section -let item = select Latex.item Html.item TeXmacs.item -let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item -let rule = select Latex.rule Html.rule TeXmacs.rule +let section = select Latex.section Html.section TeXmacs.section Raw.section +let item = select Latex.item Html.item TeXmacs.item Raw.item +let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item +let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule -let char = select Latex.char Html.char TeXmacs.char -let ident = select Latex.ident Html.ident TeXmacs.ident -let symbol = select Latex.symbol Html.symbol TeXmacs.symbol +let char = select Latex.char Html.char TeXmacs.char Raw.char +let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident +let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol -let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char +let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char let latex_string = - select Latex.latex_string Html.latex_string TeXmacs.latex_string -let html_char = select Latex.html_char Html.html_char TeXmacs.html_char + select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string +let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char let html_string = - select Latex.html_string Html.html_string TeXmacs.html_string + select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string let start_latex_math = - select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math + select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = - select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math + select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math let start_verbatim = - select Latex.start_verbatim Html.start_verbatim TeXmacs.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 + select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim let verbatim_char = - select output_char Html.char TeXmacs.char + select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char -let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index -let make_index = select Latex.make_index Html.make_index TeXmacs.make_index -let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc +let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index +let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index +let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc |