# HG changeset patch
# User wenzelm
# Date 1452269863 -3600
# Node ID 3b61d05eadadce8be188cdad493a2bebfad1e43b
# Parent  7a5754afe170fd2216cb2ac213bb9ee0587ee0e6
tuned;

diff -r 7a5754afe170 -r 3b61d05eadad src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/Pure/General/symbol.scala	Fri Jan 08 17:17:43 2016 +0100
@@ -468,14 +468,14 @@
     val control_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
-    val sub_decoded = decode("\\<^sub>")
-    val sup_decoded = decode("\\<^sup>")
+    val sub_decoded = decode(sub)
+    val sup_decoded = decode(sup)
+    val bold_decoded = decode(bold)
+    val emph_decoded = decode("\\<^emph>")
     val bsub_decoded = decode("\\<^bsub>")
     val esub_decoded = decode("\\<^esub>")
     val bsup_decoded = decode("\\<^bsup>")
     val esup_decoded = decode("\\<^esup>")
-    val bold_decoded = decode("\\<^bold>")
-    val emph_decoded = decode("\\<^emph>")
   }
 
 
@@ -557,12 +557,16 @@
   def is_controllable(sym: Symbol): Boolean =
     !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
 
+  val sub = "\\<^sub>"
+  val sup = "\\<^sup>"
+  val bold = "\\<^bold>"
+
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded
+  def bold_decoded: Symbol = symbols.bold_decoded
+  def emph_decoded: Symbol = symbols.emph_decoded
   def bsub_decoded: Symbol = symbols.bsub_decoded
   def esub_decoded: Symbol = symbols.esub_decoded
   def bsup_decoded: Symbol = symbols.bsup_decoded
   def esup_decoded: Symbol = symbols.esup_decoded
-  def bold_decoded: Symbol = symbols.bold_decoded
-  def emph_decoded: Symbol = symbols.emph_decoded
 }
diff -r 7a5754afe170 -r 3b61d05eadad src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/Pure/Isar/token.scala	Fri Jan 08 17:17:43 2016 +0100
@@ -61,7 +61,7 @@
     private def other_token(keywords: Keyword.Keywords): Parser[Token] =
     {
       val letdigs1 = many1(Symbol.is_letdig)
-      val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
+      val sub = one(s => s == Symbol.sub_decoded || s == Symbol.sub)
       val id =
         one(Symbol.is_letter) ~
           (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^