(* Title: Pure/Thy/html.ML
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_path: Url.T option -> text -> text
val para: text -> text
val preform: text -> text
val verbatim: string -> text
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 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 theory_source: text -> text
val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
(Url.T * Url.T * bool) list -> text -> text
val external_file: Url.T -> string -> text
end;
structure HTML: HTML =
struct
(** HTML print modes **)
(* mode *)
val htmlN = "HTML";
fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
(* common markup *)
fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
fun span_class (name, props) =
(case Markup.get_entity_kind (name, props) of
SOME kind => Markup.entityN ^ "_" ^ name
| NONE => name);
val _ = Markup.add_mode htmlN (span o span_class);
(* symbol output *)
local
val hidden = span Markup.hiddenN |-> enclose;
(* FIXME proper unicode -- produced on Scala side *)
val html_syms = Symtab.make
[("", (0, "")),
("\n", (0, "<br/>")),
("'", (1, "'")),
("\\<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, hidden "⇘" ^ "<sub>")),
("\\<^esub>", (0, hidden "⇙" ^ "</sub>")),
("\\<^bsup>", (0, hidden "⇗" ^ "<sup>")),
("\\<^esup>", (0, hidden "⇖" ^ "</sup>"))];
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, XML.text s));
fun output_markup (bg, en) s1 s2 =
let val (n, txt) = output_sym s2
in (n, hidden s1 ^ enclose bg en txt) end;
val output_sub = output_markup ("<sub>", "</sub>");
val output_sup = output_markup ("<sup>", "</sup>");
val output_bold = output_markup (span "bold");
fun output_syms [] (result, width) = (implode (rev result), width)
| output_syms (s1 :: rest) (result, width) =
let
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
val ((w, s), r) =
if s1 = "\\<^sub>" then (output_sub "⇩" s2, ss)
else if s1 = "\\<^isub>" then (output_sub "⇣" s2, ss)
else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss)
else if s1 = "\\<^isup>" then (output_sup "⇡" s2, ss)
else if s1 = "\\<^bold>" then (output_bold "❙" s2, ss)
else (output_sym s1, rest);
in output_syms r (s :: result, width + w) end;
in
fun output_width str = output_syms (Symbol.explode str) ([], 0);
val output = #1 o output_width;
val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
end;
(** 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=" ^ quote s ^ ">" ^ txt ^ "</a>";
fun href_path path txt = href_name (Url.implode path) 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 *)
fun begin_document title =
"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
\<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
\\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
\<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
\<head>\n\
\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
\<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
\<link media=\"all\" 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<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
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<div class=\"graphbrowser\">\n\
\<applet code=\"GraphBrowser/GraphBrowser.class\" \
\archive=\"GraphBrowser.jar\" \
\width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
\<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
\</applet>" ^ end_document)
end;
in map applet_page sizes end;
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
val theory_entry = entry;
fun session_entries [] = "</ul>"
| session_entries es =
"</ul>\n</div>\n<div class=\"sessions\">\n\
\<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
(* theory *)
val theory_source = enclose
"\n</div>\n<div class=\"source\">\n<pre>"
"</pre>\n";
local
fun file (href, path, loadit) =
href_path href (if loadit then file_path path else enclose "(" ")" (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) ^
body;
end;
(* external file *)
fun external_file path str =
begin_document ("File " ^ Url.implode path) ^
"\n</div><div class=\"external_source\">\n" ^
verbatim str ^
"\n</div>\n<div class=\"external_footer\">" ^
end_document;
end;