--- a/src/Pure/Thy/html.ML Sat Jul 07 00:15:02 2007 +0200
+++ b/src/Pure/Thy/html.ML Sat Jul 07 00:15:03 2007 +0200
@@ -7,12 +7,11 @@
signature HTML =
sig
- val output: string -> string
- val output_width: string -> string * real
- type text (* = string *)
+ 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
@@ -56,158 +55,158 @@
local
val html_syms = Symtab.make
- [("\\<spacespace>", (2.0, " ")),
- ("\\<exclamdown>", (1.0, "¡")),
- ("\\<cent>", (1.0, "¢")),
- ("\\<pounds>", (1.0, "£")),
- ("\\<currency>", (1.0, "¤")),
- ("\\<yen>", (1.0, "¥")),
- ("\\<bar>", (1.0, "¦")),
- ("\\<section>", (1.0, "§")),
- ("\\<dieresis>", (1.0, "¨")),
- ("\\<copyright>", (1.0, "©")),
- ("\\<ordfeminine>", (1.0, "ª")),
- ("\\<guillemotleft>", (1.0, "«")),
- ("\\<not>", (1.0, "¬")),
- ("\\<hyphen>", (1.0, "­")),
- ("\\<registered>", (1.0, "®")),
- ("\\<inverse>", (1.0, "¯")),
- ("\\<degree>", (1.0, "°")),
- ("\\<plusminus>", (1.0, "±")),
- ("\\<twosuperior>", (1.0, "²")),
- ("\\<threesuperior>", (1.0, "³")),
- ("\\<acute>", (1.0, "´")),
- ("\\<paragraph>", (1.0, "¶")),
- ("\\<cdot>", (1.0, "·")),
- ("\\<cedilla>", (1.0, "¸")),
- ("\\<onesuperior>", (1.0, "¹")),
- ("\\<ordmasculine>", (1.0, "º")),
- ("\\<guillemotright>", (1.0, "»")),
- ("\\<onequarter>", (1.0, "¼")),
- ("\\<onehalf>", (1.0, "½")),
- ("\\<threequarters>", (1.0, "¾")),
- ("\\<questiondown>", (1.0, "¿")),
- ("\\<times>", (1.0, "×")),
- ("\\<div>", (1.0, "÷")),
- ("\\<circ>", (1.0, "o")),
- ("\\<Alpha>", (1.0, "Α")),
- ("\\<Beta>", (1.0, "Β")),
- ("\\<Gamma>", (1.0, "Γ")),
- ("\\<Delta>", (1.0, "Δ")),
- ("\\<Epsilon>", (1.0, "Ε")),
- ("\\<Zeta>", (1.0, "Ζ")),
- ("\\<Eta>", (1.0, "Η")),
- ("\\<Theta>", (1.0, "Θ")),
- ("\\<Iota>", (1.0, "Ι")),
- ("\\<Kappa>", (1.0, "Κ")),
- ("\\<Lambda>", (1.0, "Λ")),
- ("\\<Mu>", (1.0, "Μ")),
- ("\\<Nu>", (1.0, "Ν")),
- ("\\<Xi>", (1.0, "Ξ")),
- ("\\<Omicron>", (1.0, "Ο")),
- ("\\<Pi>", (1.0, "Π")),
- ("\\<Rho>", (1.0, "Ρ")),
- ("\\<Sigma>", (1.0, "Σ")),
- ("\\<Tau>", (1.0, "Τ")),
- ("\\<Upsilon>", (1.0, "Υ")),
- ("\\<Phi>", (1.0, "Φ")),
- ("\\<Chi>", (1.0, "Χ")),
- ("\\<Psi>", (1.0, "Ψ")),
- ("\\<Omega>", (1.0, "Ω")),
- ("\\<alpha>", (1.0, "α")),
- ("\\<beta>", (1.0, "β")),
- ("\\<gamma>", (1.0, "γ")),
- ("\\<delta>", (1.0, "δ")),
- ("\\<epsilon>", (1.0, "ε")),
- ("\\<zeta>", (1.0, "ζ")),
- ("\\<eta>", (1.0, "η")),
- ("\\<theta>", (1.0, "ϑ")),
- ("\\<iota>", (1.0, "ι")),
- ("\\<kappa>", (1.0, "κ")),
- ("\\<lambda>", (1.0, "λ")),
- ("\\<mu>", (1.0, "μ")),
- ("\\<nu>", (1.0, "ν")),
- ("\\<xi>", (1.0, "ξ")),
- ("\\<omicron>", (1.0, "ο")),
- ("\\<pi>", (1.0, "π")),
- ("\\<rho>", (1.0, "ρ")),
- ("\\<sigma>", (1.0, "σ")),
- ("\\<tau>", (1.0, "τ")),
- ("\\<upsilon>", (1.0, "υ")),
- ("\\<phi>", (1.0, "φ")),
- ("\\<chi>", (1.0, "χ")),
- ("\\<psi>", (1.0, "ψ")),
- ("\\<omega>", (1.0, "ω")),
- ("\\<bullet>", (1.0, "•")),
- ("\\<dots>", (1.0, "…")),
- ("\\<Re>", (1.0, "ℜ")),
- ("\\<Im>", (1.0, "ℑ")),
- ("\\<wp>", (1.0, "℘")),
- ("\\<forall>", (1.0, "∀")),
- ("\\<partial>", (1.0, "∂")),
- ("\\<exists>", (1.0, "∃")),
- ("\\<emptyset>", (1.0, "∅")),
- ("\\<nabla>", (1.0, "∇")),
- ("\\<in>", (1.0, "∈")),
- ("\\<notin>", (1.0, "∉")),
- ("\\<Prod>", (1.0, "∏")),
- ("\\<Sum>", (1.0, "∑")),
- ("\\<star>", (1.0, "∗")),
- ("\\<propto>", (1.0, "∝")),
- ("\\<infinity>", (1.0, "∞")),
- ("\\<angle>", (1.0, "∠")),
- ("\\<and>", (1.0, "∧")),
- ("\\<or>", (1.0, "∨")),
- ("\\<inter>", (1.0, "∩")),
- ("\\<union>", (1.0, "∪")),
- ("\\<sim>", (1.0, "∼")),
- ("\\<cong>", (1.0, "≅")),
- ("\\<approx>", (1.0, "≈")),
- ("\\<noteq>", (1.0, "≠")),
- ("\\<equiv>", (1.0, "≡")),
- ("\\<le>", (1.0, "≤")),
- ("\\<ge>", (1.0, "≥")),
- ("\\<subset>", (1.0, "⊂")),
- ("\\<supset>", (1.0, "⊃")),
- ("\\<subseteq>", (1.0, "⊆")),
- ("\\<supseteq>", (1.0, "⊇")),
- ("\\<oplus>", (1.0, "⊕")),
- ("\\<otimes>", (1.0, "⊗")),
- ("\\<bottom>", (1.0, "⊥")),
- ("\\<lceil>", (1.0, "⌈")),
- ("\\<rceil>", (1.0, "⌉")),
- ("\\<lfloor>", (1.0, "⌊")),
- ("\\<rfloor>", (1.0, "⌋")),
- ("\\<langle>", (1.0, "⟨")),
- ("\\<rangle>", (1.0, "⟩")),
- ("\\<lozenge>", (1.0, "◊")),
- ("\\<spadesuit>", (1.0, "♠")),
- ("\\<clubsuit>", (1.0, "♣")),
- ("\\<heartsuit>", (1.0, "♥")),
- ("\\<diamondsuit>", (1.0, "♦")),
- ("\\<lbrakk>", (2.0, "[|")),
- ("\\<rbrakk>", (2.0, "|]")),
- ("\\<Longrightarrow>", (3.0, "==>")),
- ("\\<Rightarrow>", (2.0, "=>")),
- ("\\<And>", (2.0, "!!")),
- ("\\<Colon>", (2.0, "::")),
- ("\\<lparr>", (2.0, "(|")),
- ("\\<rparr>", (2.0, "|)),")),
- ("\\<longleftrightarrow>", (3.0, "<->")),
- ("\\<longrightarrow>", (3.0, "-->")),
- ("\\<rightarrow>", (2.0, "->")),
- ("\\<^bsub>", (0.0, "<sub>")),
- ("\\<^esub>", (0.0, "</sub>")),
- ("\\<^bsup>", (0.0, "<sup>")),
- ("\\<^esup>", (0.0, "</sup>"))];
+ [("\\<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.0, Symbol.decode_raw s)
+ if Symbol.is_raw s then (1, Symbol.decode_raw s)
else
(case Symtab.lookup html_syms s of SOME x => x
- | NONE => (real (size s), translate_string escape s));
+ | 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);
@@ -224,10 +223,10 @@
fun output_width str =
if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
- then Symbol.default_output 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.0
+ (output_syms (Symbol.explode str)) 0
in (implode syms, width) end;
val output = #1 o output_width;
@@ -236,18 +235,33 @@
end;
-(* token translations *)
+(* markup and token translations *)
+
+fun span s = ("<span class=" ^ Library.quote s ^ ">", "</span>");
+
+fun style s = apfst (span s |-> enclose) o output_width;
-fun style s =
- apfst (enclose ("<span class=" ^ Library.quote s ^ ">") "</span>") 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 Syntax.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", style "free"),
+ ("free", free_or_skolem),
("bound", style "bound"),
- ("var", style "var"),
+ ("var", var_or_skolem),
("xstr", style "xstr")];
val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans);
@@ -264,7 +278,7 @@
val plain = output;
val name = enclose "<span class=\"name\">" "</span>" o output;
val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
-val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
+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;
@@ -377,7 +391,7 @@
fun theory up A =
begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
- keyword "theory" ^ " " ^ name A;
+ command "theory" ^ " " ^ name A;
fun imports Bs =
keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
@@ -422,7 +436,7 @@
in
-fun result ctxt k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map (thm ctxt) ths));
+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);
@@ -440,7 +454,7 @@
(* mode output *)
-val _ = Output.add_mode htmlN
- (output_width, K keyword_width, Symbol.default_indent, Symbol.encode_raw);
+val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
+val _ = Pretty.add_mode htmlN Pretty.default_indent (span o #1);
end;