(* 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 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_session_index: 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 theory: string -> (Url.T option * string) list -> text -> 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 = ("", ""); val _ = Markup.add_mode htmlN (span o fst); (* symbol output *) local val hidden = span Markup.hiddenN |-> enclose; (* FIXME proper unicode -- produced on Scala side *) val html_syms = Symtab.make [("", (0, "")), ("'", (1, "'")), ("\\", (1, "¡")), ("\\", (1, "¢")), ("\\", (1, "£")), ("\\", (1, "¤")), ("\\", (1, "¥")), ("\\", (1, "¦")), ("\\", (1, "§")), ("\\", (1, "¨")), ("\\", (1, "©")), ("\\", (1, "ª")), ("\\", (1, "«")), ("\\", (1, "¬")), ("\\", (1, "")), ("\\", (1, "®")), ("\\", (1, "¯")), ("\\", (1, "°")), ("\\", (1, "±")), ("\\", (1, "´")), ("\\", (1, "¶")), ("\\", (1, "·")), ("\\", (1, "¸")), ("\\", (1, "º")), ("\\", (1, "»")), ("\\", (1, "¼")), ("\\", (1, "½")), ("\\", (1, "¾")), ("\\", (1, "¿")), ("\\", (1, "×")), ("\\", (1, "÷")), ("\\", (1, "o")), ("\\", (1, "Α")), ("\\", (1, "Β")), ("\\", (1, "Γ")), ("\\", (1, "Δ")), ("\\", (1, "Ε")), ("\\", (1, "Ζ")), ("\\", (1, "Η")), ("\\", (1, "Θ")), ("\\", (1, "Ι")), ("\\", (1, "Κ")), ("\\", (1, "Λ")), ("\\", (1, "Μ")), ("\\", (1, "Ν")), ("\\", (1, "Ξ")), ("\\", (1, "Ο")), ("\\", (1, "Π")), ("\\", (1, "Ρ")), ("\\", (1, "Σ")), ("\\", (1, "Τ")), ("\\", (1, "Υ")), ("\\", (1, "Φ")), ("\\", (1, "Χ")), ("\\", (1, "Ψ")), ("\\", (1, "Ω")), ("\\", (1, "α")), ("\\", (1, "β")), ("\\", (1, "γ")), ("\\", (1, "δ")), ("\\", (1, "ε")), ("\\", (1, "ζ")), ("\\", (1, "η")), ("\\", (1, "ϑ")), ("\\", (1, "ι")), ("\\", (1, "κ")), ("\\", (1, "λ")), ("\\", (1, "μ")), ("\\", (1, "ν")), ("\\", (1, "ξ")), ("\\", (1, "ο")), ("\\", (1, "π")), ("\\", (1, "ρ")), ("\\", (1, "σ")), ("\\", (1, "τ")), ("\\", (1, "υ")), ("\\", (1, "φ")), ("\\", (1, "χ")), ("\\", (1, "ψ")), ("\\", (1, "ω")), ("\\", (1, "•")), ("\\", (1, "…")), ("\\", (1, "℘")), ("\\", (1, "∀")), ("\\", (1, "∂")), ("\\", (1, "∃")), ("\\", (1, "∅")), ("\\", (1, "∇")), ("\\", (1, "∈")), ("\\", (1, "∉")), ("\\", (1, "∏")), ("\\", (1, "∑")), ("\\", (1, "∗")), ("\\", (1, "∝")), ("\\", (1, "∞")), ("\\", (1, "∠")), ("\\", (1, "∧")), ("\\", (1, "∨")), ("\\", (1, "∩")), ("\\", (1, "∪")), ("\\", (1, "∼")), ("\\", (1, "≅")), ("\\", (1, "≈")), ("\\", (1, "≠")), ("\\", (1, "≡")), ("\\", (1, "≤")), ("\\", (1, "≥")), ("\\", (1, "⊂")), ("\\", (1, "⊃")), ("\\", (1, "⊆")), ("\\", (1, "⊇")), ("\\", (1, "⊕")), ("\\", (1, "⊗")), ("\\", (1, "⊥")), ("\\", (1, "⌈")), ("\\", (1, "⌉")), ("\\", (1, "⌊")), ("\\", (1, "⌋")), ("\\", (1, "〈")), ("\\", (1, "〉")), ("\\", (1, "◊")), ("\\", (1, "♠")), ("\\", (1, "♣")), ("\\", (1, "♥")), ("\\", (1, "♦")), ("\\", (2, "[|")), ("\\", (2, "|]")), ("\\", (3, "==>")), ("\\", (2, "=>")), ("\\", (2, "!!")), ("\\", (2, "::")), ("\\", (2, "(|")), ("\\", (2, "|)),")), ("\\", (3, "<->")), ("\\", (3, "-->")), ("\\", (2, "->")), ("\\<^bsub>", (0, hidden "⇘" ^ "")), ("\\<^esub>", (0, hidden "⇙" ^ "")), ("\\<^bsup>", (0, hidden "⇗" ^ "")), ("\\<^esup>", (0, hidden "⇖" ^ ""))]; 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 ("", ""); val output_sup = output_markup ("", ""); 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 = "\\<^sup>" 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 "" "" o output; val keyword = enclose "" "" o output; val command = enclose "" "" o output; (* misc *) fun href_name s txt = "" ^ txt ^ ""; 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" ^ txt ^ "\n"; fun preform txt = "" ^ txt ^ ""; val verbatim = preform o output; (* document *) fun begin_document title = "\n\ \\n\ \\n\ \\n\ \\n\ \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ \\n\ \\n\ \\n\ \\n\ \\ \" ^ plain title ^ "\n"; val end_document = "\n\n\n\n"; (* session index *) fun begin_session_index session docs graph = begin_document ("Session " ^ plain session) ^ para ("View " ^ href_path graph "theory dependencies" ^ implode (map (fn (p, name) => "\nView " ^ href_path p name) docs)) ^ "\n\n\nTheories\n\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 back_link (path, name) = para (href_path path "Back" ^ " to index of " ^ plain name); 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 theory_entry (p, s) = "" ^ href_path p (plain s) ^ "\n"; (* theory *) fun theory A Bs txt = begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A ^ "\n" ^ keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^ "\n" ^ enclose "\n\n\n" "\n" txt ^ end_document; end;
" ^ txt ^ "
" "