1.1 --- a/src/Pure/Thy/html.ML	Thu Apr 17 16:30:53 2008 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Thu Apr 17 16:30:55 2008 +0200
     1.3 @@ -203,13 +203,11 @@
     1.4      ("\\<^bsup>", (0, "<sup>")),
     1.5      ("\\<^esup>", (0, "</sup>"))];
     1.6  
     1.7 -  val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
     1.8 -
     1.9    fun output_sym s =
    1.10      if Symbol.is_raw s then (1, Symbol.decode_raw s)
    1.11      else
    1.12        (case Symtab.lookup html_syms s of SOME x => x
    1.13 -      | NONE => (size s, translate_string escape s));
    1.14 +      | NONE => (size s, XML.text s));
    1.15  
    1.16    fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
    1.17    fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
    1.18 @@ -235,40 +233,17 @@
    1.19  val output = #1 o output_width;
    1.20  val output_symbols = map #2 o output_syms;
    1.21  
    1.22 +val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
    1.23 +
    1.24  end;
    1.25  
    1.26  
    1.27 -(* markup and token translations *)
    1.28 +(* common markup *)
    1.29  
    1.30 -fun span s = ("<span class=" ^ Library.quote s ^ ">", "</span>");
    1.31 +fun span s = ("<span class=" ^ Library.quote (XML.text s) ^ ">", "</span>");
    1.32  
    1.33 -fun style s = apfst (span s |-> enclose) o output_width;
    1.34 -
    1.35 -fun free_or_skolem x =
    1.36 -  (case try Name.dest_skolem x of
    1.37 -    NONE => style "free" x
    1.38 -  | SOME x' => style "skolem" x');
    1.39 -
    1.40 -fun var_or_skolem s =
    1.41 -  (case Lexicon.read_variable s of
    1.42 -    SOME (x, i) =>
    1.43 -      (case try Name.dest_skolem x of
    1.44 -        NONE => style "var" s
    1.45 -      | SOME x' => style "skolem"
    1.46 -          (setmp show_question_marks true Term.string_of_vname (x', i)))
    1.47 -  | NONE => style "var" s);
    1.48 -
    1.49 -val html_trans =
    1.50 - [("class", style "tclass"),
    1.51 -  ("tfree", style "tfree"),
    1.52 -  ("tvar",  style "tvar"),
    1.53 -  ("free",  free_or_skolem),
    1.54 -  ("bound", style "bound"),
    1.55 -  ("var",   var_or_skolem),
    1.56 -  ("xstr",  style "xstr")];
    1.57 -
    1.58 -val _ = Context.>> (Context.map_theory
    1.59 -  (Sign.add_mode_tokentrfuns htmlN html_trans));
    1.60 +val _ = Markup.add_mode htmlN (fn (name, props) =>
    1.61 +  if name = Markup.classN then span "tclass" else span name);
    1.62  
    1.63  
    1.64  
    1.65 @@ -452,10 +427,4 @@
    1.66  fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
    1.67  fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
    1.68  
    1.69 -
    1.70 -(* mode output *)
    1.71 -
    1.72 -val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
    1.73 -val _ = Markup.add_mode htmlN (span o #1);
    1.74 -
    1.75  end;