src/Tools/jEdit/src/symbols_dockable.scala
changeset 62104 fb73c0d7bb37
parent 62024 e3e22a5e85f2
child 63870 6db1aac936db
     1.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 08 17:17:43 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 08 18:18:40 2016 +0100
     1.3 @@ -17,9 +17,8 @@
     1.4  
     1.5  class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
     1.6  {
     1.7 -  private class Symbol_Component(val symbol: String, control: Boolean) extends Button
     1.8 +  private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
     1.9    {
    1.10 -    private val decoded = Symbol.decode(symbol)
    1.11      private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
    1.12  
    1.13      font =
    1.14 @@ -28,11 +27,12 @@
    1.15          case Some(font_family) => GUI.font(family = font_family, size = font_size)
    1.16        }
    1.17      action =
    1.18 -      Action(decoded) {
    1.19 +      Action(Symbol.decode(symbol)) {
    1.20          val text_area = view.getTextArea
    1.21 -        if (control && HTML.control_decoded.isDefinedAt(decoded))
    1.22 -          Token_Markup.edit_control_style(text_area, decoded)
    1.23 -        else text_area.setSelectedText(decoded)
    1.24 +        if (is_control && HTML.control.isDefinedAt(symbol))
    1.25 +          Token_Markup.edit_control_style(text_area, symbol)
    1.26 +        else
    1.27 +          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
    1.28          text_area.requestFocus
    1.29        }
    1.30      tooltip =