tuned signature;
authorwenzelm
Mon Dec 04 22:52:16 2017 +0100 (4 months ago)
changeset 67130b023f64e0d16
parent 67129 0262a378d5d6
child 67131 85d10959c2e4
tuned signature;
src/Tools/jEdit/src/isabelle_encoding.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/syntax_style.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Dec 04 21:23:56 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Dec 04 22:52:16 2017 +0100
     1.3 @@ -17,6 +17,6 @@
     1.4    def is_active(buffer: JEditBuffer): Boolean =
     1.5      buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
     1.6  
     1.7 -  def maybe_decode(buffer: JEditBuffer, s: String): String =
     1.8 +  def perhaps_decode(buffer: JEditBuffer, s: String): String =
     1.9      if (is_active(buffer)) Symbol.decode(s) else s
    1.10  }
     2.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 21:23:56 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 22:52:16 2017 +0100
     2.3 @@ -40,7 +40,7 @@
     2.4        Action(text) {
     2.5          val text_area = view.getTextArea
     2.6          val (s1, s2) =
     2.7 -          Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
     2.8 +          Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
     2.9          text_area.setSelectedText(s1 + s2)
    2.10          text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
    2.11          text_area.requestFocus
    2.12 @@ -100,7 +100,7 @@
    2.13          if (is_control && HTML.is_control(symbol))
    2.14            Syntax_Style.edit_control_style(text_area, symbol)
    2.15          else
    2.16 -          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
    2.17 +          text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
    2.18          text_area.requestFocus
    2.19        }
    2.20      tooltip =
     3.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 21:23:56 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 22:52:16 2017 +0100
     3.3 @@ -154,7 +154,7 @@
     3.4  
     3.5      val buffer = text_area.getBuffer
     3.6  
     3.7 -    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
     3.8 +    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
     3.9  
    3.10      def update_style(text: String): String =
    3.11      {