From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- tools/coqdoc/output.ml | 193 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 137 insertions(+), 56 deletions(-) (limited to 'tools/coqdoc/output.ml') diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d0bc6c2..93414f22 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Hashtbl.add token_pp s (Some l, None)) [ "*" , "\\ensuremath{\\times}"; + "|", "\\ensuremath{|}"; "->", "\\ensuremath{\\rightarrow}"; "->~", "\\ensuremath{\\rightarrow\\lnot}"; "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; @@ -153,6 +171,12 @@ module Latex = struct | _ -> output_char c + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + let latex_char = output_char let latex_string = output_string @@ -162,9 +186,14 @@ module Latex = struct 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 "\\coqdocmodule{"; + printf "\\coqlibrary{"; + label_ident !current_module; + printf "}{"; raw_ident !current_module; printf "}\n\n" end @@ -192,11 +221,53 @@ module Latex = struct with Not_found -> f tok - let ident s _ = + let module_ref m s = + printf "\\moduleid{%s}{" m; raw_ident s; printf "}" + (*i + match find_module m with + | Local -> + printf "" m; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s + i*) + + 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 -> + raw_ident s + + let defref m id ty s = + printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin - printf "\\coqdocid{"; raw_ident s; printf "}" + begin + try + (match Index.find !current_module loc with + | Def (fullid,typ) -> + defref !current_module fullid typ s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,fullid,typ) -> + ident_ref m fullid typ s + | Mod _ -> + printf "\\coqdocid{"; raw_ident s; printf "}") + with Not_found -> + if is_tactic s then begin + printf "\\coqdoctac{"; raw_ident s; printf "}" + end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end + end end let ident s l = with_latex_printing (fun s -> ident s l) s @@ -271,31 +342,51 @@ end module Html = struct let header () = - if !header_trailer then 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 + 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 self = "http://coq.inria.fr" let trailer () = if !index && !current_module <> "Index" then printf "
\n\n
\n
Index"; - if !header_trailer then begin - printf "
This page has been generated by "; - printf "coqdoc\n" self; - printf "
\n\n
\n\n\n" - end + 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 + printf "%s\n" s + done + with End_of_file -> Pervasives.close_in cin + else + begin + printf "
This page has been generated by "; + printf "coqdoc\n" self; + printf "
\n\n
\n\n\n" + end let start_module () = if not !short then begin - (* add_toc_entry (Toc_library !current_module); *) + add_toc_entry (Toc_library !current_module); printf "

Library %s

\n\n" !current_module end @@ -338,14 +429,15 @@ module Html = struct raw_ident s i*) - let ident_ref m fid s = match find_module m with - | Local -> - printf "" m fid; raw_ident s; printf "" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "" m fid; raw_ident s; printf "" - | Coqlib | Unknown -> - raw_ident s + let ident_ref m fid s = + match find_module m with + | Local -> + printf "" m fid; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m fid; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s let ident s loc = if is_keyword s then begin @@ -360,9 +452,9 @@ module Html = struct printf "" fullid; raw_ident s | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid) -> + | Ref (m,fullid,ty) -> ident_ref m fullid s - | Mod _ | Ref _ -> + | Mod _ -> raw_ident s) with Not_found -> raw_ident s @@ -429,17 +521,6 @@ module Html = struct let rule () = printf "
\n" - let entry_type = function - | Library -> "library" - | Module -> "module" - | Definition -> "definition" - | Inductive -> "inductive" - | Constructor -> "constructor" - | Lemma -> "lemma" - | Variable -> "variable" - | Axiom -> "axiom" - | TacticDefinition -> "tactic definition" - (* 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 @@ -465,7 +546,7 @@ module Html = struct if t = Library then "[library]", m ^ ".html" else - sprintf "[%s, in %s]" (entry_type t) m m , + sprintf "[%s, in %s]" (type_name t) m m , sprintf "%s.html#%s" m s) let format_bytype_index = function @@ -548,8 +629,8 @@ module Html = struct item n; printf "" r; f (); printf "\n" in - Queue.iter make_toc_entry toc_q; - stop_item (); + Queue.iter make_toc_entry toc_q; + stop_item (); end -- cgit v1.2.3