src/Tools/jEdit/src/isabelle_encoding.scala
changeset 62104 fb73c0d7bb37
parent 50203 00d8ad713e32
child 62527 aae9a2a855e0
     1.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Fri Jan 08 17:17:43 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Fri Jan 08 18:18:40 2016 +0100
     1.3 @@ -25,6 +25,9 @@
     1.4  
     1.5    def is_active(buffer: JEditBuffer): Boolean =
     1.6      buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
     1.7 +
     1.8 +  def maybe_decode(buffer: JEditBuffer, s: String): String =
     1.9 +    if (is_active(buffer)) Symbol.decode(s) else s
    1.10  }
    1.11  
    1.12  class Isabelle_Encoding extends Encoding