src/Tools/jEdit/src/symbols_dockable.scala
changeset 67130 b023f64e0d16
parent 66591 6efa351190d0
child 67389 7e21d19e7ad7
     1.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 22:52:16 2017 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4        Action(text) {
     1.5          val text_area = view.getTextArea
     1.6          val (s1, s2) =
     1.7 -          Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
     1.8 +          Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
     1.9          text_area.setSelectedText(s1 + s2)
    1.10          text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
    1.11          text_area.requestFocus
    1.12 @@ -100,7 +100,7 @@
    1.13          if (is_control && HTML.is_control(symbol))
    1.14            Syntax_Style.edit_control_style(text_area, symbol)
    1.15          else
    1.16 -          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
    1.17 +          text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
    1.18          text_area.requestFocus
    1.19        }
    1.20      tooltip =