(* Title: Pure/Thy/html.ML
ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
HTML presentation elements.
*)
signature HTML =
sig
val html_mode: ('a -> 'b) -> 'a -> 'b
type text = string
val plain: string -> text
val name: string -> text
val keyword: string -> text
val command: string -> text
val file_name: string -> text
val file_path: Url.T -> text
val href_name: string -> text -> text
val href_path: Url.T -> text -> text
val href_opt_name: string option -> text -> text
val href_opt_path: Url.T option -> text -> text
val para: text -> text
val preform: text -> text
val verbatim: string -> text
val with_charset: string -> ('a -> 'b) -> 'a -> 'b
val begin_document: string -> text
val end_document: text
val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
val end_index: text
val applet_pages: string -> Url.T * string -> (string * string) list
val theory_entry: Url.T * string -> text
val session_entries: (Url.T * string) list -> text
val verbatim_source: Symbol.symbol list -> text
val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
(Url.T option * Url.T * bool) list -> text -> text
val end_theory: text
val ml_file: Url.T -> string -> text
val results: Proof.context -> string -> (string * thm list) list -> text
val chapter: string -> text
val section: string -> text
val subsection: string -> text
val subsubsection: string -> text
end;
structure HTML: HTML =
struct
(** HTML print modes **)
(* mode *)
val htmlN = "HTML";
fun html_mode f x = PrintMode.with_modes [htmlN] f x;
(* symbol output *)
local
val html_syms = Symtab.make
[("\\<spacespace>", (2, " ")),
("\\<exclamdown>", (1, "¡")),
("\\<cent>", (1, "¢")),
("\\<pounds>", (1, "£")),
("\\<currency>", (1, "¤")),
("\\<yen>", (1, "¥")),
("\\<bar>", (1, "¦")),
("\\<section>", (1, "§")),
("\\<dieresis>", (1, "¨")),
("\\<copyright>", (1, "©")),
("\\<ordfeminine>", (1, "ª")),
("\\<guillemotleft>", (1, "«")),
("\\<not>", (1, "¬")),
("\\<hyphen>", (1, "­")),
("\\<registered>", (1, "®")),
("\\<inverse>", (1, "¯")),
("\\<degree>", (1, "°")),
("\\<plusminus>", (1, "±")),
("\\<twosuperior>", (1, "²")),
("\\<threesuperior>", (1, "³")),
("\\<acute>", (1, "´")),
("\\<paragraph>", (1, "¶")),
("\\<cdot>", (1, "·")),
("\\<cedilla>", (1, "¸")),
("\\<onesuperior>", (1, "¹")),
("\\<ordmasculine>", (1, "º")),
("\\<guillemotright>", (1, "»")),
("\\<onequarter>", (1, "¼")),
("\\<onehalf>", (1, "½")),
("\\<threequarters>", (1, "¾")),
("\\<questiondown>", (1, "¿")),
("\\<times>", (1, "×")),
("\\<div>", (1, "÷")),
("\\<circ>", (1, "o")),
("\\<Alpha>", (1, "Α")),
("\\<Beta>", (1, "Β")),
("\\<Gamma>", (1, "Γ")),
("\\<Delta>", (1, "Δ")),
("\\<Epsilon>", (1, "Ε")),
("\\<Zeta>", (1, "Ζ")),
("\\<Eta>", (1, "Η")),
("\\<Theta>", (1, "Θ")),
("\\<Iota>", (1, "Ι")),
("\\<Kappa>", (1, "Κ")),
("\\<Lambda>", (1, "Λ")),
("\\<Mu>", (1, "Μ")),
("\\<Nu>", (1, "Ν")),
("\\<Xi>", (1, "Ξ")),
("\\<Omicron>", (1, "Ο")),
("\\<Pi>", (1, "Π")),
("\\<Rho>", (1, "Ρ")),
("\\<Sigma>", (1, "Σ")),
("\\<Tau>", (1, "Τ")),
("\\<Upsilon>", (1, "Υ")),
("\\<Phi>", (1, "Φ")),
("\\<Chi>", (1, "Χ")),
("\\<Psi>", (1, "Ψ")),
("\\<Omega>", (1, "Ω")),
("\\<alpha>", (1, "α")),
("\\<beta>", (1, "β")),
("\\<gamma>", (1, "γ")),
("\\<delta>", (1, "δ")),
("\\<epsilon>", (1, "ε")),
("\\<zeta>", (1, "ζ")),
("\\<eta>", (1, "η")),
("\\<theta>", (1, "ϑ")),
("\\<iota>", (1, "ι")),
("\\<kappa>", (1, "κ")),
("\\<lambda>", (1, "λ")),
("\\<mu>", (1, "μ")),
("\\<nu>", (1, "ν")),
("\\<xi>", (1, "ξ")),
("\\<omicron>", (1, "ο")),
("\\<pi>", (1, "π")),
("\\<rho>", (1, "ρ")),
("\\<sigma>", (1, "σ")),
("\\<tau>", (1, "τ")),
("\\<upsilon>", (1, "υ")),
("\\<phi>", (1, "φ")),
("\\<chi>", (1, "χ")),
("\\<psi>", (1, "ψ")),
("\\<omega>", (1, "ω")),
("\\<bullet>", (1, "•")),
("\\<dots>", (1, "…")),
("\\<Re>", (1, "ℜ")),
("\\<Im>", (1, "ℑ")),
("\\<wp>", (1, "℘")),
("\\<forall>", (1, "∀")),
("\\<partial>", (1, "∂")),
("\\<exists>", (1, "∃")),
("\\<emptyset>", (1, "∅")),
("\\<nabla>", (1, "∇")),
("\\<in>", (1, "∈")),
("\\<notin>", (1, "∉")),
("\\<Prod>", (1, "∏")),
("\\<Sum>", (1, "∑")),
("\\<star>", (1, "∗")),
("\\<propto>", (1, "∝")),
("\\<infinity>", (1, "∞")),
("\\<angle>", (1, "∠")),
("\\<and>", (1, "∧")),
("\\<or>", (1, "∨")),
("\\<inter>", (1, "∩")),
("\\<union>", (1, "∪")),
("\\<sim>", (1, "∼")),
("\\<cong>", (1, "≅")),
("\\<approx>", (1, "≈")),
("\\<noteq>", (1, "≠")),
("\\<equiv>", (1, "≡")),
("\\<le>", (1, "≤")),
("\\<ge>", (1, "≥")),
("\\<subset>", (1, "⊂")),
("\\<supset>", (1, "⊃")),
("\\<subseteq>", (1, "⊆")),
("\\<supseteq>", (1, "⊇")),
("\\<oplus>", (1, "⊕")),
("\\<otimes>", (1, "⊗")),
("\\<bottom>", (1, "⊥")),
("\\<lceil>", (1, "⌈")),
("\\<rceil>", (1, "⌉")),
("\\<lfloor>", (1, "⌊")),
("\\<rfloor>", (1, "⌋")),
("\\<langle>", (1, "⟨")),
("\\<rangle>", (1, "⟩")),
("\\<lozenge>", (1, "◊")),
("\\<spadesuit>", (1, "♠")),
("\\<clubsuit>", (1, "♣")),
("\\<heartsuit>", (1, "♥")),
("\\<diamondsuit>", (1, "♦")),
("\\<lbrakk>", (2, "[|")),
("\\<rbrakk>", (2, "|]")),
("\\<Longrightarrow>", (3, "==>")),
("\\<Rightarrow>", (2, "=>")),
("\\<And>", (2, "!!")),
("\\<Colon>", (2, "::")),
("\\<lparr>", (2, "(|")),
("\\<rparr>", (2, "|)),")),
("\\<longleftrightarrow>", (3, "<->")),
("\\<longrightarrow>", (3, "-->")),
("\\<rightarrow>", (2, "->")),
("\\<^bsub>", (0, "<sub>")),
("\\<^esub>", (0, "</sub>")),
("\\<^bsup>", (0, "<sup>")),
("\\<^esup>", (0, "</sup>"))];
val escape = fn "<" => "<" | ">" => ">" | "&" => "&" | c => c;
fun output_sym s =
if Symbol.is_raw s then (1, Symbol.decode_raw s)
else
(case Symtab.lookup html_syms s of SOME x => x
| NONE => (size s, translate_string escape s));
fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
fun output_syms ("\\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
| output_syms ("\\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
| output_syms ("\\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
| output_syms ("\\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
| output_syms ("\\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
| output_syms (s :: ss) = output_sym s :: output_syms ss
| output_syms [] = [];
in
fun output_width str =
if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
then Output.default_output str
else
let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
(output_syms (Symbol.explode str)) 0
in (implode syms, width) end;
val output = #1 o output_width;
val output_symbols = map #2 o output_syms;
end;
(* markup and token translations *)
fun span s = ("<span class=" ^ Library.quote s ^ ">", "</span>");
fun style s = apfst (span s |-> enclose) o output_width;
fun free_or_skolem x =
(case try Name.dest_skolem x of
NONE => style "free" x
| SOME x' => style "skolem" x');
fun var_or_skolem s =
(case Lexicon.read_variable s of
SOME (x, i) =>
(case try Name.dest_skolem x of
NONE => style "var" s
| SOME x' => style "skolem"
(setmp show_question_marks true Term.string_of_vname (x', i)))
| NONE => style "var" s);
val html_trans =
[("class", style "tclass"),
("tfree", style "tfree"),
("tvar", style "tvar"),
("free", free_or_skolem),
("bound", style "bound"),
("var", var_or_skolem),
("xstr", style "xstr")];
val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
(** HTML markup **)
type text = string;
(* atoms *)
val plain = output;
val name = enclose "<span class=\"name\">" "</span>" o output;
val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
val command = enclose "<span class=\"command\">" "</span>" o output;
val file_name = enclose "<span class=\"filename\">" "</span>" o output;
val file_path = file_name o Url.implode;
(* misc *)
fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
fun href_path path txt = href_name (Url.implode path) txt;
fun href_opt_name NONE txt = txt
| href_opt_name (SOME s) txt = href_name s txt;
fun href_opt_path NONE txt = txt
| href_opt_path (SOME p) txt = href_path p txt;
fun para txt = "\n<p>" ^ txt ^ "</p>\n";
fun preform txt = "<pre>" ^ txt ^ "</pre>";
val verbatim = preform o output;
(* document *)
val charset = ref "iso-8859-1";
fun with_charset s = setmp_noncritical charset s;
fun begin_document title =
"<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \
\\"http://www.w3.org/TR/html4/loose.dtd\">\n\
\\n\
\<html>\n\
\<head>\n\
\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ ! charset ^ "\">\n\
\<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
\<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\
\</head>\n\
\\n\
\<body>\n\
\<div class=\"head\">\
\<h1>" ^ plain title ^ "</h1>\n"
val end_document = "\n</div>\n</body>\n</html>\n";
fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
val up_link = gen_link "Up";
val back_link = gen_link "Back";
(* session index *)
fun begin_index up (index_path, session) docs graph =
begin_document ("Index of " ^ session) ^ up_link up ^
para ("View " ^ href_path graph "theory dependencies" ^
implode (map (fn (p, name) => "<br>\nView " ^ href_path p name) docs)) ^
"\n</div>\n<hr>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
val end_index = end_document;
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
fun applet_pages session back =
let
val sizes =
[("small", "small.html", ("500", "400")),
("medium", "medium.html", ("650", "520")),
("large", "large.html", ("800", "640"))];
fun applet_page (size, name, (width, height)) =
let
val browser_size = "Set browser size: " ^
choice (map (fn (y, z, _) => (y, z)) sizes) size;
in
(name, begin_document ("Theory dependencies of " ^ session) ^
back_link back ^
para browser_size ^
"\n</div>\n<hr>\n<div class=\"graphbrowser\">\n\
\<applet code=\"GraphBrowser/GraphBrowser.class\" \
\archive=\"GraphBrowser.jar\" \
\width=" ^ width ^ " height=" ^ height ^ ">\n\
\<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
\</applet>\n<hr>" ^ end_document)
end;
in map applet_page sizes end;
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";
val theory_entry = entry;
fun session_entries [] = "</ul>"
| session_entries es =
"</ul>\n</div>\n<hr>\n<div class=\"sessions\">\n\
\<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
(* theory *)
fun verbatim_source ss =
"\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^
implode (output_symbols ss) ^
"</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
local
fun file (opt_ref, path, loadit) =
href_opt_path opt_ref (if loadit then enclose "(" ")" (file_path path) else file_path path);
fun theory up A =
begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
command "theory" ^ " " ^ name A;
fun imports Bs =
keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br>\n";
in
fun begin_theory up A Bs Ps body =
theory up A ^ "<br>\n" ^
imports Bs ^ "<br>\n" ^
(if null Ps then "" else uses Ps) ^
keyword "begin" ^ "<br>\n" ^
body;
end;
val end_theory = end_document;
(* ML file *)
fun ml_file path str =
begin_document ("File " ^ Url.implode path) ^
"\n</div>\n<hr><div class=\"mlsource\">\n" ^
verbatim str ^
"\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
end_document;
(* theorems *)
local
fun string_of_thm ctxt =
Output.output o Pretty.setmp_margin 80 Pretty.string_of o
setmp show_question_marks false (ProofContext.pretty_thm ctxt);
fun thm ctxt th = preform (prefix_lines " " (html_mode (string_of_thm ctxt) th));
fun thm_name "" = ""
| thm_name a = " " ^ name (a ^ ":");
in
fun result ctxt k (a, ths) = para (cat_lines ((command k ^ thm_name a) :: map (thm ctxt) ths));
fun results _ _ [] = ""
| results ctxt k (res :: ress) = cat_lines (result ctxt k res :: map (result ctxt "and") ress);
end;
(* sections *)
fun chapter heading = "\n\n<h1>" ^ plain heading ^ "</h1>\n";
fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
(* mode output *)
val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
val _ = Markup.add_mode htmlN (span o #1);
end;