# 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(_))