src/Tools/jEdit/src/token_markup.scala
changeset 62104 fb73c0d7bb37
parent 61192 98eba31c51f8
child 63421 3bf02e7fa8a3
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Fri Jan 08 17:17:43 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Fri Jan 08 18:18:40 2016 +0100
     1.3 @@ -27,26 +27,28 @@
     1.4  {
     1.5    /* editing support for control symbols */
     1.6  
     1.7 -  def update_control_style(control: String, text: String): String =
     1.8 -  {
     1.9 -    val result = new StringBuilder
    1.10 -    for (sym <- Symbol.iterator(text) if !HTML.control_decoded.isDefinedAt(sym)) {
    1.11 -      if (Symbol.is_controllable(sym)) result ++= control
    1.12 -      result ++= sym
    1.13 -    }
    1.14 -    result.toString
    1.15 -  }
    1.16 -
    1.17    def edit_control_style(text_area: TextArea, control: String)
    1.18    {
    1.19      GUI_Thread.assert {}
    1.20  
    1.21      val buffer = text_area.getBuffer
    1.22  
    1.23 +    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
    1.24 +
    1.25 +    def update_style(text: String): String =
    1.26 +    {
    1.27 +      val result = new StringBuilder
    1.28 +      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
    1.29 +        if (Symbol.is_controllable(sym)) result ++= control_decoded
    1.30 +        result ++= sym
    1.31 +      }
    1.32 +      result.toString
    1.33 +    }
    1.34 +
    1.35      text_area.getSelection.foreach(sel => {
    1.36        val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
    1.37        JEdit_Lib.try_get_text(buffer, before) match {
    1.38 -        case Some(s) if HTML.control_decoded.isDefinedAt(s) =>
    1.39 +        case Some(s) if HTML.control.isDefinedAt(s) =>
    1.40            text_area.extendSelection(before.start, before.stop)
    1.41          case _ =>
    1.42        }
    1.43 @@ -54,12 +56,11 @@
    1.44  
    1.45      text_area.getSelection.toList match {
    1.46        case Nil =>
    1.47 -        text_area.setSelectedText(control)
    1.48 +        text_area.setSelectedText(control_decoded)
    1.49        case sels =>
    1.50          JEdit_Lib.buffer_edit(buffer) {
    1.51            sels.foreach(sel =>
    1.52 -            text_area.setSelectedText(sel,
    1.53 -              update_control_style(control, text_area.getSelectedText(sel))))
    1.54 +            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
    1.55          }
    1.56      }
    1.57    }