diff options
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 100 |
1 files changed, 86 insertions, 14 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index eefcfd11..e3d5741a 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-2010 *) (* \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,7 +29,7 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; @@ -44,8 +41,7 @@ let is_keyword = "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "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"; @@ -182,10 +178,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"; @@ -306,8 +312,14 @@ 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) -> @@ -478,6 +490,8 @@ module Html = struct end let trailer () = + if !index && (get_module false) <> "Index" then + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; if !header_trailer then if !footer_file_spec then let cin = Pervasives.open_in !footer_file in @@ -489,8 +503,6 @@ module Html = struct 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>" @@ -624,7 +636,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 +674,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 +684,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 @@ -1136,6 +1193,21 @@ let verbatim_char = select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char +let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = + start_verbatim (); + 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 () + +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 |