1.1 --- a/etc/isabelle.css	Tue Jun 28 10:52:15 2011 +0200
     1.2 +++ b/etc/isabelle.css	Wed Jun 29 15:23:36 2011 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  /* basic syntax markup */
     1.6  
     1.7 -.hidden         { font-size: 0.1pt; visibility: hidden; }
     1.8 +.hidden         { font-size: 1px; visibility: hidden; }
     1.9  
    1.10  .binding        { color: #336655; }
    1.11  .entity_class   { color: red; }

     2.1 --- a/src/Pure/Thy/html.ML	Tue Jun 28 10:52:15 2011 +0200
     2.2 +++ b/src/Pure/Thy/html.ML	Wed Jun 29 15:23:36 2011 +0200
     2.3 @@ -59,8 +59,9 @@
     2.4  (* symbol output *)
     2.5  
     2.6  local
     2.7 -  val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
     2.8 +  val hidden = span Markup.hiddenN |-> enclose;
     2.9  
    2.10 +  (* FIXME proper unicode -- produced on Scala side *)
    2.11    val html_syms = Symtab.make
    2.12     [("", (0, "")),
    2.13      ("\n", (0, "<br/>")),
    2.14 @@ -205,10 +206,10 @@
    2.15      ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
    2.16      ("\\<longrightarrow>", (3, "--&gt;")),
    2.17      ("\\<rightarrow>", (2, "-&gt;")),
    2.18 -    ("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "<sub>")),
    2.19 -    ("\\<^esub>", (0, hidden "\\<^esub>" ^ "</sub>")),
    2.20 -    ("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "<sup>")),
    2.21 -    ("\\<^esup>", (0, hidden "\\<^esup>" ^ "</sup>"))];
    2.22 +    ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
    2.23 +    ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
    2.24 +    ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
    2.25 +    ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
    2.26  
    2.27    fun output_sym s =
    2.28      if Symbol.is_raw s then (1, Symbol.decode_raw s)
    2.29 @@ -224,16 +225,17 @@
    2.30    val output_sub = output_markup ("<sub>", "</sub>");
    2.31    val output_sup = output_markup ("<sup>", "</sup>");
    2.32    val output_bold = output_markup (span "bold");
    2.33 -  val output_loc = output_markup (span "loc");
    2.34  
    2.35    fun output_syms [] (result, width) = (implode (rev result), width)
    2.36      | output_syms (s1 :: rest) (result, width) =
    2.37          let
    2.38            val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
    2.39            val ((w, s), r) =
    2.40 -            if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then (output_sub s1 s2, ss)
    2.41 -            else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then (output_sup s1 s2, ss)
    2.42 -            else if s1 = "\\<^bold>" then (output_bold s1 s2, ss)
    2.43 +            if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
    2.44 +            else if s1 = "\\<^isub>" then (output_sub "&#8675;" s2, ss)
    2.45 +            else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
    2.46 +            else if s1 = "\\<^isup>" then (output_sup "&#8673;" s2, ss)
    2.47 +            else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
    2.48              else (output_sym s1, rest);
    2.49          in output_syms r (s :: result, width + w) end;
    2.50  in