src/Pure/General/symbol.scala
changeset 62103 3b61d05eadad
parent 61959 364007370bb7
child 62104 fb73c0d7bb37
     1.1 --- a/src/Pure/General/symbol.scala	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Fri Jan 08 17:17:43 2016 +0100
     1.3 @@ -468,14 +468,14 @@
     1.4      val control_decoded: Set[Symbol] =
     1.5        Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
     1.6  
     1.7 -    val sub_decoded = decode("\\<^sub>")
     1.8 -    val sup_decoded = decode("\\<^sup>")
     1.9 +    val sub_decoded = decode(sub)
    1.10 +    val sup_decoded = decode(sup)
    1.11 +    val bold_decoded = decode(bold)
    1.12 +    val emph_decoded = decode("\\<^emph>")
    1.13      val bsub_decoded = decode("\\<^bsub>")
    1.14      val esub_decoded = decode("\\<^esub>")
    1.15      val bsup_decoded = decode("\\<^bsup>")
    1.16      val esup_decoded = decode("\\<^esup>")
    1.17 -    val bold_decoded = decode("\\<^bold>")
    1.18 -    val emph_decoded = decode("\\<^emph>")
    1.19    }
    1.20  
    1.21  
    1.22 @@ -557,12 +557,16 @@
    1.23    def is_controllable(sym: Symbol): Boolean =
    1.24      !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
    1.25  
    1.26 +  val sub = "\\<^sub>"
    1.27 +  val sup = "\\<^sup>"
    1.28 +  val bold = "\\<^bold>"
    1.29 +
    1.30    def sub_decoded: Symbol = symbols.sub_decoded
    1.31    def sup_decoded: Symbol = symbols.sup_decoded
    1.32 +  def bold_decoded: Symbol = symbols.bold_decoded
    1.33 +  def emph_decoded: Symbol = symbols.emph_decoded
    1.34    def bsub_decoded: Symbol = symbols.bsub_decoded
    1.35    def esub_decoded: Symbol = symbols.esub_decoded
    1.36    def bsup_decoded: Symbol = symbols.bsup_decoded
    1.37    def esup_decoded: Symbol = symbols.esup_decoded
    1.38 -  def bold_decoded: Symbol = symbols.bold_decoded
    1.39 -  def emph_decoded: Symbol = symbols.emph_decoded
    1.40  }