diff options
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 292 |
1 files changed, 217 insertions, 75 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index eefcfd11..0dc86bc8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Cdglobals open Index @@ -32,24 +29,27 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; - "Export"; "Fact"; "Fix"; "Fixpoint"; "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"; "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"; - "Boxed"; "Unboxed"; "Inline"; + "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; "Implicit Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; - "subgoal"; - "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"; @@ -57,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"; @@ -73,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 *) @@ -118,9 +126,12 @@ let initialize_texmacs () = let token_tree_texmacs = ref (initialize_texmacs ()) +let token_tree_latex = ref Tokens.empty_ttree +let token_tree_html = ref Tokens.empty_ttree + let initialize_tex_html () = let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in - List.fold_right (fun (s,l,l') (tt,tt') -> + let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') -> (Tokens.ttree_add tt s l, match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l')) [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; @@ -143,10 +154,9 @@ let initialize_tex_html () = "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"; (* "fun", "\\ensuremath{\\lambda}" ? *) - ] (Tokens.empty_ttree,Tokens.empty_ttree) - -let token_tree_latex = ref (fst (initialize_tex_html ())) -let token_tree_html = ref (snd (initialize_tex_html ())) + ] (Tokens.empty_ttree,Tokens.empty_ttree) in + token_tree_latex := tree_latex; + token_tree_html := tree_html let add_printing_token s (t1,t2) = (match t1 with None -> () | Some t1 -> @@ -182,10 +192,20 @@ module Latex = struct let push_in_preamble s = Queue.add s preamble + let utf8x_extra_support () = + printf "\n"; + printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n"; + printf "%%interpret utf8 characters but extra packages might have to be added\n"; + printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n"; + printf "%%Use coqdoc's option -p to add new packages.\n"; + printf "\\usepackage{tipa}\n"; + printf "\n" + let header () = if !header_trailer then begin printf "\\documentclass[12pt]{report}\n"; if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; + if !inputenc = "utf8x" then utf8x_extra_support (); printf "\\usepackage[T1]{fontenc}\n"; printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; @@ -255,6 +275,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; @@ -276,9 +302,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 @@ -287,9 +327,6 @@ module Latex = struct let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space - let module_ref m s = - printf "\\coqdocmodule{%s}{%s}" m (escaped s) - let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with @@ -306,18 +343,20 @@ module Latex = struct printf "\\coqdoc%s{%s}" (type_name typ) s let defref m id ty s = - printf "\\coqdef{"; label_ident (m ^ "." ^ id); - printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s + if ty <> Notation then + (printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s) + else + (* Glob file still not able to say the exact extent of the definition *) + (* so we currently renounce to highlight the notation location *) + (printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{%s}" s s) let reference s = function | Def (fullid,typ) -> defref (get_module false) 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{%s}" (escaped s) (*s The sublexer buffers symbol characters and attached uninterpreted ident and try to apply special translation such as, @@ -330,13 +369,22 @@ 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 () = + initialize_tex_html (); Tokens.token_tree := token_tree_latex; Tokens.outfun := output_sublexer_string @@ -345,7 +393,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 @@ -478,8 +530,7 @@ module Html = struct end let trailer () = - if !header_trailer then - if !footer_file_spec then + if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file in try while true do @@ -487,14 +538,14 @@ module Html = struct printf "%s\n" s done with End_of_file -> Pervasives.close_in cin - else - begin - if !index && (get_module false) <> "Index" then - printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; - printf "<hr/>This page has been generated by "; - printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; - printf "</div>\n\n</div>\n\n</body>\n</html>" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; + printf "<hr/>This page has been generated by "; + printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; + printf "</div>\n\n</div>\n\n</body>\n</html>" + end let start_module () = let ln = !lib_name in @@ -547,17 +598,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 module_ref m s = - match find_module m with - | Local -> - printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s - | External m when !externals -> - printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s - | External _ | Unknown -> - output_string s + 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 ident_ref m fid typ s = match find_module m with @@ -575,12 +631,8 @@ module Html = struct | Def (fullid,ty) -> printf "<a name=\"%s\">" fullid; printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s - | Mod _ -> - printf "<span class=\"id\" type=\"mod\">%s</span>" s let output_sublexer_string doescape issymbchar tag s = let s = if doescape then escaped s else s in @@ -597,12 +649,16 @@ module Html = struct Tokens.output_tagged_symbol_char tag c let initialize () = + initialize_tex_html(); Tokens.token_tree := token_tree_html; Tokens.outfun := output_sublexer_string 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) @@ -624,7 +680,7 @@ module Html = struct let rec reach_item_level n = if !item_level < n then begin - printf "<ul>\n<li>"; incr item_level; + printf "<ul class=\"doclist\">\n<li>"; incr item_level; reach_item_level n end else if !item_level > n then begin printf "\n</li>\n</ul>\n"; decr item_level; @@ -662,7 +718,9 @@ module Html = struct let end_code () = end_coq (); start_doc () - let start_inline_coq () = printf "<span class=\"inlinecode\">" + let start_inline_coq () = + if !inline_notmono then printf "<span class=\"inlinecodenm\">" + else printf "<span class=\"inlinecode\">" let end_inline_coq () = printf "</span>" @@ -670,7 +728,50 @@ module Html = struct let end_inline_coq_block () = end_inline_coq () - let paragraph () = printf "\n<br/> <br/>\n" + let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" + + (* inference rules *) + let inf_rule assumptions (_,_,midnm) conclusions = + (* this first function replaces any occurance of 3 or more spaces + in a row with " "s. We do this to the assumptions so that + people can put multiple rules on a line with nice formatting *) + let replace_spaces str = + let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in + let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in + let strs = List.map (fun r -> match r with + | Str.Text s -> [s] + | Str.Delim s -> + copy " " (String.length s)) + results + in + String.concat "" (List.concat strs) + in + let start_assumption line = + (printf "<tr class=\"infruleassumption\">\n"; + printf " <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in + let end_assumption () = + (printf " <td></td>\n"; + printf "</td>\n") in + let rec print_assumptions hyps = + match hyps with + | [] -> start_assumption " " + | [(_,hyp)] -> start_assumption hyp + | ((_,hyp) :: hyps') -> (start_assumption hyp; + end_assumption (); + print_assumptions hyps') in + printf "<center><table class=\"infrule\">\n"; + print_assumptions assumptions; + printf " <td class=\"infrulenamecol\" rowspan=\"3\">\n"; + (match midnm with + | None -> printf " \n </td>" + | Some s -> printf " %s \n </td>" s); + printf "</tr>\n"; + printf "<tr class=\"infrulemiddle\">\n"; + printf " <td class=\"infrule\"><hr /></td>\n"; + printf "</tr>\n"; + print_assumptions conclusions; + end_assumption (); + printf "</table></center>" let section lev f = let lab = new_label () in @@ -858,19 +959,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 url addr name = + printf "%s<\\footnote><\\url>%s</url></footnote>" addr + (match name with + | None -> "" + | Some n -> n) - let stop_verbatim () = in_doc := false; printf "</verbatim>" + 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 = @@ -985,13 +1095,21 @@ module Raw = struct let start_latex_math () = () let stop_latex_math () = () - let start_verbatim () = () + let start_verbatim inline = () + let stop_verbatim inline = () - let stop_verbatim () = () + let url addr name = + match name with + | Some n -> printf "%s (%s)" n addr + | None -> printf "%s" addr + + 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 @@ -1105,6 +1223,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 @@ -1132,10 +1251,33 @@ 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 false; + let dumb_line = + function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln); + char '\n') + in + (List.iter dumb_line assumptions; + dumb_line (midsp, midln ^ (match midnm with + | Some s -> " " ^ s + | None -> "")); + List.iter dumb_line conclusions); + stop_verbatim false + +let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb + 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 |