src/Pure/Thy/html.scala
changeset 62104 fb73c0d7bb37
parent 60215 5fb4990dfc73
child 62113 16de2a9b5b3d
     1.1 --- a/src/Pure/Thy/html.scala	Fri Jan 08 17:17:43 2016 +0100
     1.2 +++ b/src/Pure/Thy/html.scala	Fri Jan 08 18:18:40 2016 +0100
     1.3 @@ -11,9 +11,13 @@
     1.4  {
     1.5    /* encode text with control symbols */
     1.6  
     1.7 -  val control_decoded =
     1.8 -    Map(Symbol.sub_decoded -> "sub",
     1.9 +  val control =
    1.10 +    Map(
    1.11 +      Symbol.sub -> "sub",
    1.12 +      Symbol.sub_decoded -> "sub",
    1.13 +      Symbol.sup -> "sup",
    1.14        Symbol.sup_decoded -> "sup",
    1.15 +      Symbol.bold -> "b",
    1.16        Symbol.bold_decoded -> "b")
    1.17  
    1.18    def encode(text: String): String =
    1.19 @@ -32,23 +36,23 @@
    1.20        }
    1.21      def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
    1.22  
    1.23 -    var control = ""
    1.24 +    var ctrl = ""
    1.25      for (sym <- Symbol.iterator(text)) {
    1.26 -      if (control_decoded.isDefinedAt(sym)) control = sym
    1.27 +      if (control.isDefinedAt(sym)) ctrl = sym
    1.28        else {
    1.29 -        control_decoded.get(control) match {
    1.30 +        control.get(ctrl) match {
    1.31            case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
    1.32              result ++= ("<" + elem + ">")
    1.33              encode_chars(sym)
    1.34              result ++= ("</" + elem + ">")
    1.35            case _ =>
    1.36 -            encode_chars(control)
    1.37 +            encode_chars(ctrl)
    1.38              encode_chars(sym)
    1.39          }
    1.40 -        control = ""
    1.41 +        ctrl = ""
    1.42        }
    1.43      }
    1.44 -    encode_chars(control)
    1.45 +    encode_chars(ctrl)
    1.46  
    1.47      result.toString
    1.48    }