# HG changeset patch
# User wenzelm
# Date 1512424336 -3600
# Node ID b023f64e0d162e6518c2e23ec03f04136b91b1a3
# Parent  0262a378d5d6e223c903144eb148b0e88cf05f0c
tuned signature;

diff -r 0262a378d5d6 -r b023f64e0d16 src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Dec 04 21:23:56 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Dec 04 22:52:16 2017 +0100
@@ -17,6 +17,6 @@
   def is_active(buffer: JEditBuffer): Boolean =
     buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
 
-  def maybe_decode(buffer: JEditBuffer, s: String): String =
+  def perhaps_decode(buffer: JEditBuffer, s: String): String =
     if (is_active(buffer)) Symbol.decode(s) else s
 }
diff -r 0262a378d5d6 -r b023f64e0d16 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 21:23:56 2017 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 22:52:16 2017 +0100
@@ -40,7 +40,7 @@
       Action(text) {
         val text_area = view.getTextArea
         val (s1, s2) =
-          Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
+          Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
         text_area.setSelectedText(s1 + s2)
         text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
         text_area.requestFocus
@@ -100,7 +100,7 @@
         if (is_control && HTML.is_control(symbol))
           Syntax_Style.edit_control_style(text_area, symbol)
         else
-          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
+          text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
         text_area.requestFocus
       }
     tooltip =
diff -r 0262a378d5d6 -r b023f64e0d16 src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 21:23:56 2017 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 22:52:16 2017 +0100
@@ -154,7 +154,7 @@
 
     val buffer = text_area.getBuffer
 
-    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
+    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
 
     def update_style(text: String): String =
     {