src/Tools/jEdit/src/syntax_style.scala
changeset 67130 b023f64e0d16
parent 67128 4d91b6d5d49c
     1.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 18:30:28 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 22:52:16 2017 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  
     1.5      val buffer = text_area.getBuffer
     1.6  
     1.7 -    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
     1.8 +    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
     1.9  
    1.10      def update_style(text: String): String =
    1.11      {