", (1.0, "÷")),
("\\", (1.0, "o")),
("\\", (1.0, "Α")),
("\\", (1.0, "Β")),
("\\", (1.0, "Γ")),
("\\", (1.0, "Δ")),
("\\", (1.0, "Ε")),
("\\", (1.0, "Ζ")),
("\\", (1.0, "Η")),
("\\", (1.0, "Θ")),
("\\", (1.0, "Ι")),
("\\", (1.0, "Κ")),
("\\", (1.0, "Λ")),
("\\", (1.0, "Μ")),
("\\", (1.0, "Ν")),
("\\", (1.0, "Ξ")),
("\\", (1.0, "Ο")),
("\\", (1.0, "Π")),
("\\", (1.0, "Ρ")),
("\\", (1.0, "Σ")),
("\\", (1.0, "Τ")),
("\\", (1.0, "Υ")),
("\\", (1.0, "Φ")),
("\\", (1.0, "Χ")),
("\\", (1.0, "Ψ")),
("\\", (1.0, "Ω")),
("\\", (1.0, "α")),
("\\", (1.0, "β")),
("\\", (1.0, "γ")),
("\\", (1.0, "δ")),
("\\", (1.0, "ε")),
("\\", (1.0, "ζ")),
("\\", (1.0, "η")),
("\\", (1.0, "ϑ")),
("\\", (1.0, "ι")),
("\\", (1.0, "κ")),
("\\", (1.0, "λ")),
("\\", (1.0, "μ")),
("\\", (1.0, "ν")),
("\\", (1.0, "ξ")),
("\\", (1.0, "ο")),
("\\", (1.0, "π")),
("\\", (1.0, "ρ")),
("\\", (1.0, "σ")),
("\\", (1.0, "τ")),
("\\", (1.0, "υ")),
("\\", (1.0, "φ")),
("\\", (1.0, "χ")),
("\\", (1.0, "ψ")),
("\\", (1.0, "ω")),
("\\", (1.0, "•")),
("\\", (1.0, "…")),
("\\", (1.0, "ℜ")),
("\\", (1.0, "ℑ")),
("\\", (1.0, "℘")),
("\\", (1.0, "∀")),
("\\", (1.0, "∂")),
("\\", (1.0, "∃")),
("\\", (1.0, "∅")),
("\\", (1.0, "∇")),
("\\", (1.0, "∈")),
("\\", (1.0, "∉")),
("\\", (1.0, "∏")),
("\\", (1.0, "∑")),
("\\", (1.0, "∗")),
("\\", (1.0, "∝")),
("\\", (1.0, "∞")),
("\\", (1.0, "∠")),
("\\", (1.0, "∧")),
("\\", (1.0, "∨")),
("\\", (1.0, "∩")),
("\\", (1.0, "∪")),
("\\", (1.0, "∼")),
("\\", (1.0, "≅")),
("\\", (1.0, "≈")),
("\\", (1.0, "≠")),
("\\", (1.0, "≡")),
("\\", (1.0, "≤")),
("\\", (1.0, "≥")),
("\\", (1.0, "⊂")),
("\\", (1.0, "⊃")),
("\\", (1.0, "⊆")),
("\\", (1.0, "⊇")),
("\\", (1.0, "⊕")),
("\\", (1.0, "⊗")),
("\\", (1.0, "⊥")),
("\\", (1.0, "⌈")),
("\\", (1.0, "⌉")),
("\\", (1.0, "⌊")),
("\\", (1.0, "⌋")),
("\\", (1.0, "〈")),
("\\", (1.0, "〉")),
("\\", (1.0, "◊")),
("\\", (1.0, "♠")),
("\\", (1.0, "♣")),
("\\", (1.0, "♥")),
("\\", (1.0, "♦")),
("\\", (2.0, "[|")),
("\\", (2.0, "|]")),
("\\", (3.0, "==>")),
("\\", (2.0, "=>")),
("\\", (2.0, "!!")),
("\\", (2.0, "::")),
("\\", (2.0, "(|")),
("\\", (2.0, "|)),")),
("\\", (3.0, "<->")),
("\\", (3.0, "-->")),
("\\", (2.0, "->")),
("\\<^bsub>", (0.0, "")),
("\\<^esub>", (0.0, "")),
("\\<^bsup>", (0.0, "")),
("\\<^esup>", (0.0, ""))];
val escape = fn "<" => "<" | ">" => ">" | "&" => "&" | c => c;
fun output_sym s =
if Symbol.is_raw s then (1.0, Symbol.decode_raw s)
else
(case Symtab.lookup html_syms s of SOME x => x
| NONE => (real (size s), translate_string escape s));
fun output_sub s = apsnd (enclose "" "") (output_sym s);
fun output_sup s = apsnd (enclose "" "") (output_sym s);
fun output_loc s = apsnd (enclose "" "") (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 Symbol.default_output str
else
let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
(output_syms (Symbol.explode str)) 0.0
in (implode syms, width) end;
val output = #1 o output_width;
val output_symbols = map #2 o output_syms;
end;
(* token translations *)
fun style s =
apfst (enclose ("") "") o output_width;
val html_trans =
[("class", style "tclass"),
("tfree", style "tfree"),
("tvar", style "tvar"),
("free", style "free"),
("bound", style "bound"),
("var", style "var"),
("xstr", style "xstr")];
val _ = Context.add_setup (Theory.add_mode_tokentrfuns htmlN html_trans);
(** HTML markup **)
type text = string;
(* atoms *)
val plain = output;
val name = enclose "" "" o output;
val keyword = enclose "" "" o output;
val keyword_width = apfst (enclose "" "") o output_width;
val file_name = enclose "" "" o output;
val file_path = file_name o Url.pack;
(* misc *)
fun href_name s txt = "" ^ txt ^ "";
fun href_path path txt = href_name (Url.pack 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
" ^ txt ^ "
\n";
fun preform txt = "
" ^ txt ^ "
";
val verbatim = preform o output;
(* document *)
val charset = ref "iso-8859-1";
fun with_charset s = setmp charset s;
fun begin_document title =
"\n\
\\n\
\\n\
\\n\
\\n\
\" ^ plain (title ^ " (" ^ version ^ ")") ^ "\n\
\\n\
\\n\
\\n\
\\n\
\
\
\
" ^ plain title ^ "
\n"
val end_document = "\n
\n\n\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) => " \nView " ^ href_path p name) docs)) ^
"\n
\n\n
\n
Theories
\n
\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
\n\n
\n\
\\n" ^ end_document)
end;
in map applet_page sizes end;
fun entry (p, s) = "
" ^ href_path p (plain s) ^ "\n";
val theory_entry = entry;
fun session_entries [] = ""
| session_entries es =
"\n
\n\n
\n\
\
Sessions
\n
\n" ^ implode (map entry es) ^ "
";
(* theory *)
fun verbatim_source ss =
"\n
\n\n
\n
" ^
implode (output_symbols ss) ^
"
\n
\n\n
\n";
local
fun encl NONE = enclose "[" "]"
| encl (SOME false) = enclose "(" ")"
| encl (SOME true) = I;
fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path));
fun theory up A =
begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
keyword "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) ^ " \n";
in
fun begin_theory up A Bs Ps body =
theory up A ^ " \n" ^
imports Bs ^ " \n" ^
(if null Ps then "" else uses Ps) ^
keyword "begin" ^ " \n" ^
body;
end;
val end_theory = end_document;
(* ML file *)
fun ml_file path str =
begin_document ("File " ^ Url.pack path) ^
"\n