(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* Hashtbl.add h key ()) l; function s -> try Hashtbl.find h s; true with Not_found -> false 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"; "Guarded"; "Goal"; "Hint"; "Debug"; "On"; "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; "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"; "SearchHead"; "SearchPattern"; "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"; "subgoals"; "vm_compute"; "Opaque"; "Transparent"; "Time"; "Extraction"; "Extract"; "Variant"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; "Program Instance"; "Equations"; "Equations_nocomp"; (*i (* coq terms *) *) "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; "fix"; "cofix"; "is"; (* Ltac *) "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec"; (* Notations *) "level"; "associativity"; "no" ] let is_tactic = build_table [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; "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"; "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"; "fail"; "fresh"; "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 *) let current_module : (string * string option) ref = ref ("",None) 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 let in_doc = ref false (*s Customized and predefined pretty-print *) let initialize_texmacs () = let ensuremath x = sprintf ">" 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 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 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 "×"; "|", "\\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}" ? *) ] (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 -> 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 * string option | Toc_section of int * (unit -> unit) * string let (toc_q : toc_entry Queue.t) = Queue.create () let add_toc_entry e = Queue.add e toc_q let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r (*s LaTeX output *) module Latex = struct let in_title = ref false (*s Latex preamble *) let (preamble : string Queue.t) = Queue.create () 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 "%%such as \"textgreek\" for Greek letters not already in tipa\n"; printf "%%or \"stmaryrd\" for mathematical symbols.\n"; printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n"; printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n"; printf "%%Use coqdoc's option -p to add new packages or declarations.\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"; printf "\\usepackage{amsmath,amssymb}\n"; printf "\\usepackage{url}\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 "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"; output_string "%% This file has been automatically generated with the command\n"; output_string "%% "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf "\n"; output_string "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n" let trailer () = if !header_trailer then begin 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 ' ' | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '^' | '~' -> 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 let html_char _ = () let html_string _ = () (*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 "{}" | '\'' -> 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; 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 '$' let stop_latex_math () = output_char '$' 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 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 printf "\\coqdocnoindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with | Local -> 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 = 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 | Ref (m,fullid,typ) -> ident_ref m fullid typ 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 last_was_in = ref false let sublexer c loc = 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 sublexer_in_doc c = if c = '*' && !last_was_in then begin Tokens.flush_sublexer (); output_char '*' end else Tokens.output_tagged_symbol_char None c; last_was_in := false let initialize () = initialize_tex_html (); 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 keyword s loc = printf "\\coqdockw{%s}" (translate s) let ident s loc = last_was_in := s = "in"; try match loc with | None -> raise Not_found | Some loc -> 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 let tag = Index.find_string s in reference (translate s) tag with _ -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s let ident s l = if !in_title then ( printf "\\texorpdfstring{\\protect"; ident s l; printf "}{%s}" (translate s)) else ident s l (*s Translating structure *) let proofbox () = printf "\\ensuremath{\\Box}" 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 end else if !item_level > n then begin printf "\n\\end{itemize}\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; if n <= old_level then printf "\n\\item " let stop_item () = reach_item_level 0 let start_doc () = in_doc := true let end_doc () = in_doc := false; stop_item () (* 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" let end_comment () = printf "\\end{coqdoccomment}\n" let start_coq () = printf "\\begin{coqdoccode}\n" let end_coq () = printf "\\end{coqdoccode}\n" let start_code () = end_doc (); start_coq () let end_code () = end_coq (); start_doc () let section_kind = function | 1 -> "\\section{" | 2 -> "\\subsection{" | 3 -> "\\subsubsection{" | 4 -> "\\paragraph{" | _ -> assert false let section lev f = stop_item (); output_string (section_kind lev); in_title := true; f (); in_title := false; printf "}\n\n" let rule () = printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" 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 () = () let make_multi_index () = () let make_index () = () let make_toc () = printf "\\tableofcontents\n" end (*s HTML output *) module Html = struct let header () = 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 printf "%s\n" s done with End_of_file -> Pervasives.close_in cin else begin printf "\n"; printf "\n\n"; printf "\n" !charset; printf "\n"; printf "%s\n\n\n" !page_title; printf "\n\n
\n\n
\n
\n\n"; printf "
\n\n" end let trailer () = if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file 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 else begin if !index && (get_module false) <> "Index" then printf "
\n\n
\n
Index" !index_name; printf "
This page has been generated by "; printf "coqdoc\n" Coq_config.wwwcoq; printf "
\n\n
\n\n\n" end let start_module () = let ln = !lib_name in if not !short then begin let (m,sub) = !current_module in add_toc_entry (Toc_library (m,sub)); if ln = "" then printf "

%s

\n\n" (get_module true) else printf "

%s %s

\n\n" ln (get_module true) end let indentation n = for _i = 1 to n do printf " " done let line_break () = printf "
\n" let empty_line_of_code () = printf "\n
\n" let nbsp () = printf " " let char = function | '<' -> printf "<" | '>' -> printf ">" | '&' -> printf "&" | c -> output_char c 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 "&" | '\"' -> Buffer.add_string buff """ | c -> Buffer.add_char buff c done; Buffer.contents buff let sanitize_name s = let rec loop esc i = if i < 0 then if esc then escaped s else s else match s.[i] with | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1) | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1) | _ -> (* This name contains complex characters: this is probably a notation string, we simply hash it. *) Digest.to_hex (Digest.string s) in loop false (String.length s - 1) let latex_char _ = () let latex_string _ = () let html_char = output_char let html_string = output_string let start_latex_math () = () let stop_latex_math () = () let start_quote () = char '"' let stop_quote () = start_quote () let start_verbatim inline = if inline then printf "" else printf "
"

  let stop_verbatim inline = 
    if inline then printf "" 
    else printf "
\n" let url addr name = printf "%s" addr (match name with | Some n -> n | None -> addr) let ident_ref m fid typ s = match find_module m with | Local -> printf "" m (sanitize_name fid); printf "%s" typ s | External m when !externals -> printf "" m (sanitize_name fid); printf "%s" typ s | External _ | Unknown -> printf "%s" typ s let reference s r = match r with | Def (fullid,ty) -> printf "" (sanitize_name fullid); printf "%s" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) 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 "%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 sublexer_in_doc c = Tokens.output_tagged_symbol_char None 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 "%s" (translate s) let ident s loc = try match loc with | None -> raise Not_found | Some loc -> reference (translate s) (Index.find (get_module false) loc) with Not_found -> if is_tactic s then printf "%s" (translate s) else if is_keyword s then printf "%s" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try reference (translate s) (Index.find_string s) with Not_found -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s let proofbox () = printf "☐" let rec reach_item_level n = if !item_level < n then begin printf "\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; if n <= old_level then printf "\n\n
  • " let stop_item () = reach_item_level 0 let start_coq () = if not !raw_comments then printf "
    \n" let end_coq () = if not !raw_comments then printf "
    \n" let start_doc () = in_doc := true; if not !raw_comments then printf "\n
    \n" let end_doc () = in_doc := false; stop_item (); if not !raw_comments then printf "\n
    \n" let start_emph () = printf "" let stop_emph () = printf "" let start_comment () = printf "(*" let end_comment () = printf "*)" let start_code () = end_doc (); start_coq () let end_code () = end_coq (); start_doc () let start_inline_coq () = if !inline_notmono then printf "" else printf "" let end_inline_coq () = printf "" let start_inline_coq_block () = line_break (); start_inline_coq () let end_inline_coq_block () = end_inline_coq () let paragraph () = printf "\n
    \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 "\n"; printf " %s\n" (replace_spaces line)) in let end_assumption () = (printf " \n"; printf "\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 "
    \n"; print_assumptions assumptions; printf " " | Some s -> printf " %s  \n " s); printf "\n"; printf "\n"; printf " \n"; printf "\n"; print_assumptions conclusions; end_assumption (); printf "
    \n"; (match midnm with | None -> printf "  \n
    " let section lev f = let lab = new_label () in 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 "" lab lev; f (); printf "\n" lev let rule () = printf "
    \n" (* 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 !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 "

    %s %s

    \n" idx c (display_letter c) cat; List.iter (fun (id,(text,link,t)) -> let id' = prepare_entry id t in printf "%s %s
    \n" link id' text) l; printf "

    " 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 let ln = !lib_name in if ln <> "" then "[" ^ lowercase ln ^ "]", m ^ ".html", t else "[library]", m ^ ".html", t else sprintf "[%s, in %s]" (type_name t) m m , sprintf "%s.html#%s" m (sanitize_name s), t) let format_bytype_index = function | Library, idx -> Index.map (fun id m -> "", m ^ ".html", Library) idx | (t,idx) -> Index.map (fun s m -> let text = sprintf "[in %s]" m m in (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx (* Impression de la table d'index *) let print_index_table_item i = printf "\n%s Index\n" (capitalize i.idx_name); List.iter (fun (c,l) -> if l <> [] then printf "%s\n" (index_ref i c) (display_letter c) else printf "%s\n" (display_letter c)) i.idx_entries; let n = i.idx_size in printf "(%d %s)\n" n (if n > 1 then "entries" else "entry"); printf "\n" let print_index_table idxl = printf "\n"; List.iter print_index_table_item idxl; printf "
    \n" let make_one_multi_index prt_tbl i = (* 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 "%s_%s_%c.html" !index_name idx c); if (!header_trailer) then header (); prt_tbl (); printf "
    "; letter_index true idx cl; if List.length l > 30 then begin printf "
    "; prt_tbl () end; if (!header_trailer) then trailer (); close_out_file () in List.iter one_letter i.idx_entries 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 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 let print_one_index i = if i.idx_size > 0 then begin printf "
    \n

    %s Index

    \n" (capitalize i.idx_name); all_letters i end in set_module "Index" None; if !title <> "" then printf "

    %s

    \n" !title; print_table (); if not (!multi_index) then begin List.iter print_one_index all_index; printf "
    "; print_table () end 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 "

    %s

    \n" m ms else printf "

    %s %s

    \n" m ln ms | Toc_section (n, f, r) -> item n; printf "" r; f (); printf "\n" in printf "
    \n"; Queue.iter make_toc_entry toc_q; stop_item (); printf "
    \n" end (*s TeXmacs-aware output *) module TeXmacs = struct (*s Latex preamble *) let (_ : string Queue.t) = in_doc := false; Queue.create () let header () = output_string "(*i This file has been automatically generated with the command \n"; 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 "\\<" | '|' -> printf "\\|" | '>' -> printf "\\>" | _ -> output_char c let char c = if !in_doc then char_true c else output_char c let latex_char = char_true let latex_string = String.iter latex_char 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 start_latex_math () = printf "' let start_verbatim inline = in_doc := true; printf "<\\verbatim>" let stop_verbatim inline = in_doc := false; printf "" let url addr name = printf "%s<\\footnote><\\url>%s" 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 "" let ident_true s = 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 = 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 sublexer_in_doc c = 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"; incr item_level; reach_item_level n end else if !item_level > n then begin printf "\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; if n <= old_level then printf "\n\n" let stop_item () = reach_item_level 0 let start_doc () = in_doc := true; printf "(** texmacs: " let end_doc () = stop_item (); in_doc := false; printf " *)" let start_coq () = () let end_coq () = () let start_emph () = printf "" let start_comment () = () let end_comment () = () let start_code () = in_doc := true; printf "<\\code>\n" let end_code () = in_doc := false; printf "\n" let section_kind = function | 1 -> "section" | 2 -> "subsection" | 3 -> "subsubsection" | 4 -> "paragraph" | _ -> assert false let section lev f = stop_item (); printf "<"; output_string (section_kind lev); printf "|"; f (); printf ">\n\n" let rule () = printf "\n\n" let paragraph () = printf "\n\n" let line_break () = printf "\n" let empty_line_of_code () = printf "\n" let start_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 () = () let make_toc () = () end (*s Raw output *) module Raw = struct let header () = () let trailer () = () let nbsp () = output_char ' ' let char = output_char 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 start_latex_math () = () let stop_latex_math () = () 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 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 let sublexer_in_doc c = char c 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_emph () = printf "_" let stop_emph () = printf "_" let start_comment () = printf "(*" let end_comment () = printf "*)" 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 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 () = () end (*s Generic output *) 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 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 Raw.start_module 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_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment 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 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 Raw.start_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 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 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 sublexer_in_doc = select Latex.sublexer_in_doc Html.sublexer_in_doc TeXmacs.sublexer_in_doc Raw.sublexer_in_doc 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 = 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 Raw.html_string 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 = 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 Raw.start_verbatim let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim 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