diff options
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 759 |
1 files changed, 456 insertions, 303 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 1ad8b14f..93e1f843 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 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) open Cdglobals open Index @@ -25,26 +25,26 @@ let sprintf = Printf.sprintf (*s Coq keywords *) -let build_table l = +let build_table l = let h = Hashtbl.create 101 in List.iter (fun key ->Hashtbl.add h key ()) l; function s -> try Hashtbl.find h s; true with Not_found -> false -let is_keyword = +let is_keyword = build_table [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; - "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + "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"; + "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"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; + "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"; + "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; "Implicit Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; @@ -54,13 +54,13 @@ let is_keyword = "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; "Program Instance"; "Equations"; "Equations_nocomp"; (*i (* coq terms *) *) - "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; + "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; (* Ltac *) "before"; "after" ] -let is_tactic = +let is_tactic = build_table [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; @@ -77,30 +77,51 @@ let is_tactic = (*s Current Coq module *) -let current_module = ref "" +let current_module : (string * string option) ref = ref ("",None) -let set_module m = current_module := m; page_title := m +let get_module withsub = + let (m,sub) = !current_module in + if withsub then + match sub with + | None -> m + | Some sub -> m ^ ": " ^ sub + else + m + +let set_module m sub = current_module := (m,sub); + page_title := get_module true (*s Common to both LaTeX and HTML *) let item_level = ref 0 - -(*s Customized pretty-print *) - -let token_pp = Hashtbl.create 97 - -let add_printing_token = Hashtbl.replace token_pp - -let find_printing_token tok = - try Hashtbl.find token_pp tok with Not_found -> None, None - -let remove_printing_token = Hashtbl.remove token_pp - -(* predefined pretty-prints *) -let initialize () = +let in_doc = ref false + +(*s Customized and predefined pretty-print *) + +let initialize_texmacs () = + let ensuremath x = sprintf "<with|mode|math|\\<%s\\>>" x in + List.fold_right (fun (s,t) tt -> Tokens.ttree_add tt s t) + [ "*", ensuremath "times"; + "->", ensuremath "rightarrow"; + "<-", ensuremath "leftarrow"; + "<->", ensuremath "leftrightarrow"; + "=>", ensuremath "Rightarrow"; + "<=", ensuremath "le"; + ">=", ensuremath "ge"; + "<>", ensuremath "noteq"; + "~", ensuremath "lnot"; + "/\\", ensuremath "land"; + "\\/", ensuremath "lor"; + "|-", ensuremath "vdash" + ] Tokens.empty_ttree + +let token_tree_texmacs = ref (initialize_texmacs ()) + +let initialize_tex_html () = 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')) + 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 "×"; "|", "\\ensuremath{|}", None; "->", "\\ensuremath{\\rightarrow}", if_utf8 "→"; @@ -119,14 +140,27 @@ let initialize () = "forall", "\\ensuremath{\\forall}", if_utf8 "∀"; "exists", "\\ensuremath{\\exists}", if_utf8 "∃"; "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; - "λ", "\\ensuremath{\\lambda}", 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 ())) + +let add_printing_token s (t1,t2) = + (match t1 with None -> () | Some t1 -> + token_tree_latex := Tokens.ttree_add !token_tree_latex s t1); + (match t2 with None -> () | Some t2 -> + token_tree_html := Tokens.ttree_add !token_tree_html s t2) + +let remove_printing_token s = + token_tree_latex := Tokens.ttree_remove !token_tree_latex s; + token_tree_html := Tokens.ttree_remove !token_tree_html s (*s Table of contents *) -type toc_entry = - | Toc_library of string +type toc_entry = + | Toc_library of string * string option | Toc_section of int * (unit -> unit) * string let (toc_q : toc_entry Queue.t) = Queue.create () @@ -140,7 +174,6 @@ 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 *) @@ -155,10 +188,14 @@ module Latex = struct printf "\\usepackage[T1]{fontenc}\n"; printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; + printf "\\usepackage{amsmath,amssymb}\n"; + (match !toc_depth with + | None -> () + | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n); Queue.iter (fun s -> printf "%s\n" s) preamble; printf "\\begin{document}\n" end; - output_string + output_string "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"; output_string "%% This file has been automatically generated with the command\n"; @@ -173,21 +210,28 @@ module Latex = struct printf "\\end{document}\n" end + (*s Latex low-level translation *) + + let nbsp () = output_char '~' + let char c = match c with - | '\\' -> + | '\\' -> printf "\\symbol{92}" - | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> + | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> output_char '\\'; output_char c - | '^' | '~' -> + | '^' | '~' -> output_char '\\'; output_char c; printf "{}" - | _ -> + | _ -> output_char c let label_char c = match c with - | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' - | '^' | '~' -> () - | _ -> - output_char c + | '_' -> output_char ' ' + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' + | '^' | '~' -> printf "x%X" (Char.code c) + | _ -> if c >= '\x80' then printf "x%X" (Char.code c) else output_char c + + let label_ident s = + for i = 0 to String.length s - 1 do label_char s.[i] done let latex_char = output_char let latex_string = output_string @@ -195,19 +239,36 @@ module Latex = struct let html_char _ = () let html_string _ = () - let raw_ident s = - for i = 0 to String.length s - 1 do char s.[i] done - - let label_ident s = - for i = 0 to String.length s - 1 do label_char s.[i] done - - let start_module () = - if not !short then begin - printf "\\coqlibrary{"; - label_ident !current_module; - printf "}{"; - raw_ident !current_module; - printf "}\n\n" + (*s Latex char escaping *) + + let escaped = + let buff = Buffer.create 5 in + fun s -> + Buffer.clear buff; + for i = 0 to String.length s - 1 do + match s.[i] with + | '\\' -> + Buffer.add_string buff "\\symbol{92}" + | '$' | '#' | '%' | '&' | '{' | '}' | '_' as c -> + Buffer.add_char buff '\\'; Buffer.add_char buff c + | '^' | '~' as c -> + Buffer.add_char buff '\\'; Buffer.add_char buff c; + Buffer.add_string buff "{}" + | c -> + Buffer.add_char buff c + done; + Buffer.contents buff + + (*s Latex reference and symbol translation *) + + let start_module () = + let ln = !lib_name in + if not !short then begin + printf "\\coqlibrary{"; + label_ident (get_module false); + printf "}{"; + if ln <> "" then printf "%s " ln; + printf "}{%s}\n\n" (escaped (get_module true)) end let start_latex_math () = output_char '$' @@ -218,89 +279,101 @@ module Latex = struct let stop_verbatim () = printf "\\end{verbatim}\n" - let indentation n = - if n == 0 then + let indentation n = + if n == 0 then printf "\\coqdocnoindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space - let with_latex_printing f tok = - try - (match Hashtbl.find token_pp tok with - | Some s, _ -> output_string s - | _ -> f tok) - with Not_found -> - f tok - - let module_ref m s = - printf "\\moduleid{%s}{" m; raw_ident s; printf "}" - (*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 module_ref m s = + printf "\\moduleid{%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 | Local -> - printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" - | Coqlib when !externals -> - let _m = Filename.concat !coqlib m in - printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" - | Coqlib | Unknown -> - printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" + if typ = Variable then + printf "\\coqdoc%s{%s}" (type_name typ) s + else + (printf "\\coqref{"; label_ident id; + printf "}{\\coqdoc%s{%s}}" (type_name typ) s) + | External m when !externals -> + printf "\\coqexternalref{"; label_ident fid; + printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s + | External _ | Unknown -> + printf "\\coqdoc%s{%s}" (type_name typ) s let defref m id ty s = - printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s let reference s = function - | Def (fullid,typ) -> - defref !current_module fullid typ s + | Def (fullid,typ) -> + defref (get_module false) fullid typ s | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid,typ) -> + | 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 + printf "\\coqdocvar{%s}" (escaped s) + + (*s The sublexer buffers symbol characters and attached + uninterpreted ident and try to apply special translation such as, + predefined, translation "->" to "\ensuremath{\rightarrow}" or, + virtually, a user-level translation from "=_h" to "\ensuremath{=_{h}}" *) + + let output_sublexer_string doescape issymbchar tag s = + let s = if doescape then escaped s else s in + match tag with + | Some ref -> reference s ref + | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s + + 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 + + let initialize () = + Tokens.token_tree := token_tree_latex; + Tokens.outfun := output_sublexer_string + + (*s Interpreting ident with fallback on sublexer if unknown ident *) + + let translate s = + match Tokens.translate s with Some s -> s | None -> escaped s + + let ident s loc = + try + let tag = Index.find (get_module false) loc in + reference (translate s) tag + with Not_found -> + if is_tactic s then + printf "\\coqdoctac{%s}" (translate s) + else if is_keyword s then + printf "\\coqdockw{%s}" (translate s) + else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + then try - 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 - 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 tag = Index.find_string (get_module false) s in + reference (translate s) tag + with _ -> Tokens.output_tagged_ident_string s + else Tokens.output_tagged_ident_string s - let ident s l = + let ident s l = if !in_title then ( printf "\\texorpdfstring{\\protect"; - with_latex_printing (fun s -> ident s l) s; - printf "}{"; raw_ident s; printf "}") + ident s l; + printf "}{%s}" (translate s)) else - with_latex_printing (fun s -> ident s l) s - - let symbol s = with_latex_printing raw_ident s + ident s l + + (*s Translating structure *) + + let proofbox () = printf "\\ensuremath{\\Box}" - let rec reach_item_level n = + let rec reach_item_level n = if !item_level < n then begin printf "\n\\begin{itemize}\n\\item "; incr item_level; reach_item_level n @@ -320,7 +393,11 @@ module Latex = struct let end_doc () = in_doc := false; stop_item () - let comment c = char c + (* This is broken if we are in math mode, but coqdoc currently isn't + tracking that *) + let start_emph () = printf "\\textit{" + + let stop_emph () = printf "}" let start_comment () = printf "\\begin{coqdoccomment}\n" @@ -350,12 +427,16 @@ module Latex = struct let rule () = printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" - let paragraph () = stop_item (); printf "\n\n" + let paragraph () = printf "\n\n" let line_break () = printf "\\coqdoceol\n" let empty_line_of_code () = printf "\\coqdocemptyline\n" + let start_inline_coq_block () = line_break (); empty_line_of_code () + + let end_inline_coq_block () = empty_line_of_code () + let start_inline_coq () = () let end_inline_coq () = () @@ -377,9 +458,9 @@ module Html = struct if !header_trailer then if !header_file_spec then let cin = Pervasives.open_in !header_file in - try - while true do - let s = Pervasives.input_line cin in + try + while true do + let s = Pervasives.input_line cin in printf "%s\n" s done with End_of_file -> Pervasives.close_in cin @@ -396,14 +477,14 @@ module Html = struct end let trailer () = - if !index && !current_module <> "Index" then - printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>"; - if !header_trailer then + 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 - try - while true do - let s = Pervasives.input_line cin in + try + while true do + let s = Pervasives.input_line cin in printf "%s\n" s done with End_of_file -> Pervasives.close_in cin @@ -414,26 +495,47 @@ module Html = struct printf "</div>\n\n</div>\n\n</body>\n</html>" end - let start_module () = + let start_module () = + let ln = !lib_name in if not !short then begin - add_toc_entry (Toc_library !current_module); - printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module + let (m,sub) = !current_module in + add_toc_entry (Toc_library (m,sub)); + if ln = "" then + printf "<h1 class=\"libtitle\">%s</h1>\n\n" (get_module true) + else + printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true) end let indentation n = for i = 1 to n do printf " " done let line_break () = printf "<br/>\n" - let empty_line_of_code () = + let empty_line_of_code () = printf "\n<br/>\n" + let nbsp () = printf " " + let char = function | '<' -> printf "<" | '>' -> printf ">" | '&' -> printf "&" | c -> output_char c - let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + let raw_string s = + for i = 0 to String.length s - 1 do char s.[i] done + + let escaped = + let buff = Buffer.create 5 in + fun s -> + Buffer.clear buff; + for i = 0 to String.length s - 1 do + match s.[i] with + | '<' -> Buffer.add_string buff "<" + | '>' -> Buffer.add_string buff ">" + | '&' -> Buffer.add_string buff "&" + | c -> Buffer.add_char buff c + done; + Buffer.contents buff let latex_char _ = () let latex_string _ = () @@ -447,74 +549,81 @@ module Html = struct let start_verbatim () = printf "<pre>" let stop_verbatim () = printf "</pre>\n" - let module_ref m s = + let module_ref m s = match find_module m with | Local -> - 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=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" - | Coqlib | Unknown -> - raw_ident s + 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 ident_ref m fid typ s = match find_module m with | Local -> printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; - printf "<span class=\"id\" type=\"%s\">" typ; - raw_ident s; - printf "</span></a>" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; - printf "<span class=\"id\" type=\"%s\">" typ; - raw_ident s; printf "</span></a>" - | 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=\"id\" type=\"keyword\">"; - raw_ident s; - printf "</span>" - end else - begin - try - (match Index.find !current_module loc with - | Def (fullid,ty) -> - printf "<a name=\"%s\">" fullid; - printf "<span class=\"id\" type=\"%s\">" (type_name ty); - raw_ident s; printf "</span></a>" - | 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\">"; raw_ident s ; printf "</span>") - with Not_found -> - 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 + printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s + | External m when !externals -> + printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; + printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s + | External _ | Unknown -> + printf "<span class=\"id\" type=\"%s\">%s</span>" typ s + + let reference s r = + match r with + | 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 + match tag with + | Some ref -> reference s ref + | None -> + if issymbchar then output_string s + else printf "<span class=\"id\" type=\"var\">%s</span>" s + + 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 - let with_html_printing f tok = - try - (match Hashtbl.find token_pp tok with - | _, Some s -> output_string s - | _ -> f tok) - with Not_found -> - f tok + let initialize () = + Tokens.token_tree := token_tree_html; + Tokens.outfun := output_sublexer_string - let ident s l = - with_html_printing (fun s -> ident s l) s + let translate s = + match Tokens.translate s with Some s -> s | None -> escaped s - let symbol s = - with_html_printing raw_ident s + let ident s loc = + if is_keyword s then begin + printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s) + end else begin + try reference (translate s) (Index.find (get_module false) loc) + with Not_found -> + if is_tactic s then + printf "<span class=\"id\" type=\"tactic\">%s</span>" (translate s) + else + if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + then + try reference (translate s) (Index.find_string (get_module false) s) + with _ -> Tokens.output_tagged_ident_string s + else + Tokens.output_tagged_ident_string s + end - let rec reach_item_level n = + let proofbox () = printf "<font size=-2>☐</font>" + + let rec reach_item_level n = if !item_level < n then begin - printf "\n<ul>\n<li>"; incr item_level; + printf "<ul>\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; @@ -532,14 +641,18 @@ module Html = struct let end_coq () = if not !raw_comments then printf "</div>\n" - let start_doc () = + let start_doc () = in_doc := true; if not !raw_comments then printf "\n<div class=\"doc\">\n" - let end_doc () = - stop_item (); + let end_doc () = in_doc := false; + stop_item (); if not !raw_comments then printf "\n</div>\n" + let start_emph () = printf "<i>" + + let stop_emph () = printf "</i>" + let start_comment () = printf "<span class=\"comment\">(*" let end_comment () = printf "*)</span>" @@ -552,16 +665,19 @@ module Html = struct let end_inline_coq () = printf "</span>" - let paragraph () = - let i = !item_level in - stop_item (); - if i > 0 then printf "\n" - else printf "\n<br/> <br/>\n" + let start_inline_coq_block () = line_break (); start_inline_coq () + + let end_inline_coq_block () = end_inline_coq () + + let paragraph () = printf "\n<br/> <br/>\n" let section lev f = let lab = new_label () in - let r = sprintf "%s.html#%s" !current_module lab in - add_toc_entry (Toc_section (lev, f, r)); + let r = sprintf "%s.html#%s" (get_module false) lab in + (match !toc_depth with + | None -> add_toc_entry (Toc_section (lev, f, r)) + | Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r)) + else ()); stop_item (); printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev; f (); @@ -572,64 +688,70 @@ module Html = struct (* make a HTML index from a list of triples (name,text,link) *) let index_ref i c = let idxc = sprintf "%s_%c" i.idx_name c in - if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc + !index_name ^ (if !multi_index then "_" ^ idxc ^ ".html" else ".html#" ^ idxc) let letter_index category idx (c,l) = if l <> [] then begin let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in - printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat; - List.iter - (fun (id,(text,link)) -> - printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l; + printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; + List.iter + (fun (id,(text,link,t)) -> + let id' = prepare_entry id t in + printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l; printf "<br/><br/>" end - + 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) *) let format_global_index = - Index.map - (fun s (m,t) -> - if t = Library then - "[library]", m ^ ".html" - else - sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m , - sprintf "%s.html#%s" m s) + Index.map + (fun s (m,t) -> + if t = Library then + let ln = !lib_name in + if ln <> "" then + "[" ^ String.lowercase ln ^ "]", m ^ ".html", t + else + "[library]", m ^ ".html", t + else + sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m , + sprintf "%s.html#%s" m s, t) let format_bytype_index = function | Library, idx -> - Index.map (fun id m -> "", m ^ ".html") idx + Index.map (fun id m -> "", m ^ ".html", Library) idx | (t,idx) -> - Index.map - (fun s m -> + Index.map + (fun s m -> let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in - (text, sprintf "%s.html#%s" m s)) idx + (text, sprintf "%s.html#%s" m s, t)) idx (* Impression de la table d'index *) let print_index_table_item i = printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name); - List.iter - (fun (c,l) -> + List.iter + (fun (c,l) -> if l <> [] then - printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c + printf "<td><a href=\"%s\">%s</a></td>\n" (index_ref i c) + (display_letter c) else - printf "<td>%c</td>\n" c) + printf "<td>%s</td>\n" (display_letter c)) i.idx_entries; let n = i.idx_size in printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry"); printf "</tr>\n" - let print_index_table idxl = + let print_index_table idxl = printf "<table>\n"; List.iter print_index_table_item idxl; 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ée 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); + open_out_file (sprintf "%s_%s_%c.html" !index_name idx c); if (!header_trailer) then header (); prt_tbl (); printf "<hr/>"; letter_index true idx cl; @@ -639,16 +761,16 @@ module Html = struct in List.iter one_letter i.idx_entries - let make_multi_index () = - let all_index = + let make_multi_index () = + let all_index = let glob,bt = Index.all_entries () in (format_global_index glob) :: (List.map format_bytype_index bt) in let print_table () = print_index_table all_index in List.iter (make_one_multi_index print_table) all_index - + let make_index () = - let all_index = + let all_index = let glob,bt = Index.all_entries () in (format_global_index glob) :: (List.map format_bytype_index bt) in @@ -659,26 +781,33 @@ module Html = struct all_letters i end in - current_module := "Index"; + set_module "Index" None; if !title <> "" then printf "<h1>%s</h1>\n" !title; print_table (); - if not (!multi_index) then + if not (!multi_index) then begin List.iter print_one_index all_index; printf "<hr/>"; print_table () end - - let make_toc () = - let make_toc_entry = function - | Toc_library m -> - stop_item (); - printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m - | Toc_section (n, f, r) -> - item n; - printf "<a href=\"%s\">" r; f (); printf "</a>\n" - in - Queue.iter make_toc_entry toc_q; - stop_item (); + + let make_toc () = + let ln = !lib_name in + let make_toc_entry = function + | Toc_library (m,sub) -> + stop_item (); + let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in + if ln = "" then + printf "<a href=\"%s.html\"><h2>%s</h2></a>\n" m ms + else + printf "<a href=\"%s.html\"><h2>%s %s</h2></a>\n" m ln ms + | Toc_section (n, f, r) -> + item n; + printf "<a href=\"%s\">" r; f (); printf "</a>\n" + in + printf "<div id=\"toc\">\n"; + Queue.iter make_toc_entry toc_q; + stop_item (); + printf "</div>\n" end @@ -689,21 +818,21 @@ module TeXmacs = struct (*s Latex preamble *) - let in_doc = ref false - - let (preamble : string Queue.t) = + let (preamble : string Queue.t) = in_doc := false; Queue.create () let push_in_preamble s = Queue.add s preamble let header () = - output_string + output_string "(*i This file has been automatically generated with the command \n"; - output_string + output_string " "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n" let trailer () = () + let nbsp () = output_char ' ' + let char_true c = match c with | '\\' -> printf "\\\\" | '<' -> printf "\\<" @@ -734,7 +863,7 @@ module TeXmacs = struct let indentation n = () - let ident_true s = + let ident_true s = if is_keyword s then begin printf "<kw|"; raw_ident s; printf ">" end else begin @@ -742,27 +871,20 @@ module TeXmacs = struct end let ident s _ = if !in_doc then ident_true s else raw_ident s - - let symbol_true s = - let ensuremath x = printf "<with|mode|math|\\<%s\\>>" x in - match s with - | "*" -> ensuremath "times" - | "->" -> ensuremath "rightarrow" - | "<-" -> ensuremath "leftarrow" - | "<->" ->ensuremath "leftrightarrow" - | "=>" -> ensuremath "Rightarrow" - | "<=" -> ensuremath "le" - | ">=" -> ensuremath "ge" - | "<>" -> ensuremath "noteq" - | "~" -> ensuremath "lnot" - | "/\\" -> ensuremath "land" - | "\\/" -> ensuremath "lor" - | "|-" -> ensuremath "vdash" - | s -> raw_ident s - - let symbol s = if !in_doc then symbol_true s else raw_ident s - - let rec reach_item_level n = + + let output_sublexer_string doescape issymbchar tag s = + if doescape then raw_ident s else output_string s + + let sublexer c l = + if !in_doc then Tokens.output_tagged_symbol_char None c else char c + + let initialize () = + Tokens.token_tree := token_tree_texmacs; + Tokens.outfun := output_sublexer_string + + let proofbox () = printf "QED" + + let rec reach_item_level n = if !item_level < n then begin printf "\n<\\itemize>\n<item>"; incr item_level; reach_item_level n @@ -786,6 +908,9 @@ module TeXmacs = struct let end_coq () = () + let start_emph () = printf "<with|font shape|italic|" + let stop_emph () = printf ">" + let start_comment () = () let end_comment () = () @@ -801,13 +926,13 @@ module TeXmacs = struct let section lev f = stop_item (); - printf "<"; output_string (section_kind lev); printf "|"; + printf "<"; output_string (section_kind lev); printf "|"; f (); printf ">\n\n" let rule () = printf "\n<hrule>\n" - let paragraph () = stop_item (); printf "\n\n" + let paragraph () = printf "\n\n" let line_break_true () = printf "<format|line break>" @@ -819,6 +944,10 @@ module TeXmacs = struct let end_inline_coq () = printf "]>" + let start_inline_coq_block () = line_break (); start_inline_coq () + + let end_inline_coq_block () = end_inline_coq () + let make_multi_index () = () let make_index () = () @@ -828,7 +957,7 @@ module TeXmacs = struct end -(*s LaTeX output *) +(*s Raw output *) module Raw = struct @@ -836,13 +965,9 @@ module Raw = struct let trailer () = () - let char = output_char + let nbsp () = output_char ' ' - let label_char c = match c with - | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' - | '^' | '~' -> () - | _ -> - output_char c + let char = output_char let latex_char = output_char let latex_string = output_string @@ -863,22 +988,31 @@ module Raw = struct let stop_verbatim () = () - let indentation n = + let indentation n = for i = 1 to n do printf " " done let ident s loc = raw_ident s - let symbol s = raw_ident s + let sublexer c l = char c - let item n = printf "- " + let initialize () = + Tokens.token_tree := ref Tokens.empty_ttree; + Tokens.outfun := (fun _ _ _ _ -> failwith "Useless") + + let proofbox () = printf "[]" + let item n = printf "- " let stop_item () = () + let reach_item_level _ = () let start_doc () = printf "(** " let end_doc () = printf " *)\n" - let start_comment () = () - let end_comment () = () + let start_emph () = printf "_" + let stop_emph () = printf "_" + + let start_comment () = printf "(*" + let end_comment () = printf "*)" let start_coq () = () let end_coq () = () @@ -886,15 +1020,15 @@ module Raw = struct let start_code () = end_doc (); start_coq () let end_code () = end_coq (); start_doc () - let section_kind = + let section_kind = function - | 1 -> "*" - | 2 -> "**" - | 3 -> "***" - | 4 -> "****" - | _ -> assert false + | 1 -> "* " + | 2 -> "** " + | 3 -> "*** " + | 4 -> "**** " + | _ -> assert false - let section lev f = + let section lev f = output_string (section_kind lev); f () @@ -909,9 +1043,12 @@ module Raw = struct let start_inline_coq () = () let end_inline_coq () = () + let start_inline_coq_block () = line_break (); start_inline_coq () + let end_inline_coq_block () = end_inline_coq () + let make_multi_index () = () let make_index () = () - let make_toc () = () + let make_toc () = () end @@ -919,7 +1056,7 @@ end (*s Generic output *) -let select f1 f2 f3 f4 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 @@ -927,7 +1064,7 @@ let push_in_preamble = Latex.push_in_preamble 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 = +let 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 Raw.start_doc @@ -940,45 +1077,61 @@ let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.star 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 Raw.start_code -let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code -let start_inline_coq = +let start_inline_coq = select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq -let end_inline_coq = +let end_inline_coq = select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq +let start_inline_coq_block = + select Latex.start_inline_coq_block Html.start_inline_coq_block + TeXmacs.start_inline_coq_block Raw.start_inline_coq_block +let end_inline_coq_block = + select Latex.end_inline_coq_block Html.end_inline_coq_block TeXmacs.end_inline_coq_block Raw.end_inline_coq_block + 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 +let empty_line_of_code = select 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 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 reach_item_level = select Latex.reach_item_level Html.reach_item_level TeXmacs.reach_item_level Raw.reach_item_level 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 ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident -let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol +let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer +let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize + +let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char -let latex_string = +let latex_string = 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 = +let html_string = select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string -let start_latex_math = +let start_emph = + select Latex.start_emph Html.start_emph TeXmacs.start_emph Raw.start_emph +let stop_emph = + select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph + +let start_latex_math = select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math -let stop_latex_math = +let stop_latex_math = select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math -let start_verbatim = +let start_verbatim = select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim -let stop_verbatim = +let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim -let verbatim_char = +let verbatim_char = select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char |