1.1 --- a/etc/isabelle.css	Sun Jun 19 14:36:06 2011 +0200
     1.2 +++ b/etc/isabelle.css	Sun Jun 19 15:22:58 2011 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4  .inner_comment, inner_comment { color: #8B0000; }
     1.5  
     1.6  .bold, bold  { font-weight: bold; }
     1.7 -.loc, loc  { color: #D2691E; }
     1.8  
     1.9  .keyword, keyword      { font-weight: bold; }
    1.10  .operator, operator    { }

     2.1 --- a/lib/texinputs/isabelle.sty	Sun Jun 19 14:36:06 2011 +0200
     2.2 +++ b/lib/texinputs/isabelle.sty	Sun Jun 19 15:22:58 2011 +0200
     2.3 @@ -37,7 +37,6 @@
     2.4  \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
     2.5  \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
     2.6  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
     2.7 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
     2.8  
     2.9  \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    2.10  \newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}

     3.1 --- a/src/Pure/Thy/html.ML	Sun Jun 19 14:36:06 2011 +0200
     3.2 +++ b/src/Pure/Thy/html.ML	Sun Jun 19 15:22:58 2011 +0200
     3.3 @@ -229,7 +229,6 @@
     3.4              if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then (output_sub s1 s2, ss)
     3.5              else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then (output_sup s1 s2, ss)
     3.6              else if s1 = "\\<^bold>" then (output_bold s1 s2, ss)
     3.7 -            else if s1 = "\\<^loc>" then (output_loc s1 s2, ss)
     3.8              else (output_sym s1, rest);
     3.9          in output_syms r (s :: result, width + w) end;
    3.10  in

     4.1 --- a/src/Pure/Thy/html.scala	Sun Jun 19 14:36:06 2011 +0200
     4.2 +++ b/src/Pure/Thy/html.scala	Sun Jun 19 15:22:58 2011 +0200
     4.3 @@ -86,7 +86,6 @@
     4.4              else if (symbols.is_bold_decoded(s1)) {
     4.5                add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
     4.6              }
     4.7 -            else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
     4.8              else t ++= s1
     4.9            }
    4.10            flush()

     5.1 --- a/src/Tools/WWW_Find/html_unicode.ML	Sun Jun 19 14:36:06 2011 +0200
     5.2 +++ b/src/Tools/WWW_Find/html_unicode.ML	Sun Jun 19 15:22:58 2011 +0200
     5.3 @@ -51,13 +51,11 @@
     5.4  
     5.5    fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
     5.6    fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
     5.7 -  fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
     5.8  
     5.9    fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
    5.10      | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
    5.11      | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
    5.12      | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
    5.13 -    | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
    5.14      | output_syms (s :: ss) = output_sym s :: output_syms ss
    5.15      | output_syms [] = [];
    5.16  

     6.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 14:36:06 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 15:22:58 2011 +0200
     6.3 @@ -32,7 +32,7 @@
     6.4    {
     6.5      if (Isabelle.extended_styles) {
     6.6        // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
     6.7 -      // FIXME \\<^bold> \\<^loc>
     6.8 +      // FIXME \\<^bold>
     6.9        def ctrl_style(sym: String): Option[Byte => Byte] =
    6.10          if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
    6.11          else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))