# HG changeset patch
# User wenzelm
# Date 1308489778 -7200
# Node ID b55a273ede187d36af7310620cce3e20d620a356
# Parent  fe539d5177501dee2d111c75d9632a37831c84f2
discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);

diff -r fe539d517750 -r b55a273ede18 etc/isabelle.css
--- a/etc/isabelle.css	Sun Jun 19 14:36:06 2011 +0200
+++ b/etc/isabelle.css	Sun Jun 19 15:22:58 2011 +0200
@@ -33,7 +33,6 @@
 .inner_comment, inner_comment { color: #8B0000; }
 
 .bold, bold  { font-weight: bold; }
-.loc, loc  { color: #D2691E; }
 
 .keyword, keyword      { font-weight: bold; }
 .operator, operator    { }
diff -r fe539d517750 -r b55a273ede18 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sun Jun 19 14:36:06 2011 +0200
+++ b/lib/texinputs/isabelle.sty	Sun Jun 19 15:22:58 2011 +0200
@@ -37,7 +37,6 @@
 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
-\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 \newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
diff -r fe539d517750 -r b55a273ede18 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sun Jun 19 14:36:06 2011 +0200
+++ b/src/Pure/Thy/html.ML	Sun Jun 19 15:22:58 2011 +0200
@@ -229,7 +229,6 @@
             if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then (output_sub s1 s2, ss)
             else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then (output_sup s1 s2, ss)
             else if s1 = "\\<^bold>" then (output_bold s1 s2, ss)
-            else if s1 = "\\<^loc>" then (output_loc s1 s2, ss)
             else (output_sym s1, rest);
         in output_syms r (s :: result, width + w) end;
 in
diff -r fe539d517750 -r b55a273ede18 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Jun 19 14:36:06 2011 +0200
+++ b/src/Pure/Thy/html.scala	Sun Jun 19 15:22:58 2011 +0200
@@ -86,7 +86,6 @@
             else if (symbols.is_bold_decoded(s1)) {
               add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
             }
-            else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
             else t ++= s1
           }
           flush()
diff -r fe539d517750 -r b55a273ede18 src/Tools/WWW_Find/html_unicode.ML
--- a/src/Tools/WWW_Find/html_unicode.ML	Sun Jun 19 14:36:06 2011 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML	Sun Jun 19 15:22:58 2011 +0200
@@ -51,13 +51,11 @@
 
   fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
   fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
-  fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
 
   fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
     | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
     | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
     | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
-    | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
     | output_syms (s :: ss) = output_sym s :: output_syms ss
     | output_syms [] = [];
 
diff -r fe539d517750 -r b55a273ede18 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 14:36:06 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 15:22:58 2011 +0200
@@ -32,7 +32,7 @@
   {
     if (Isabelle.extended_styles) {
       // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
-      // FIXME \\<^bold> \\<^loc>
+      // FIXME \\<^bold>
       def ctrl_style(sym: String): Option[Byte => Byte] =
         if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
         else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))