# 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 "" "") (output_sym s);
fun output_sup s = apsnd (enclose "" "") (output_sym s);
- fun output_loc s = apsnd (enclose "" "") (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(_))