tuned;
authorwenzelm
Sun Mar 24 18:30:59 2019 +0100 (4 weeks ago)
changeset 69969c211db89f916
parent 69968 1a400b14fd3a
child 69970 b5a47478897a
tuned;
src/Tools/jEdit/src/syntax_style.scala
     1.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Sun Mar 24 17:53:46 2019 +0100
     1.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Sun Mar 24 18:30:59 2019 +0100
     1.3 @@ -148,13 +148,13 @@
     1.4  
     1.5    /* editing support for control symbols */
     1.6  
     1.7 -  def edit_control_style(text_area: TextArea, control: String)
     1.8 +  def edit_control_style(text_area: TextArea, control_sym: String)
     1.9    {
    1.10      GUI_Thread.assert {}
    1.11  
    1.12      val buffer = text_area.getBuffer
    1.13  
    1.14 -    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
    1.15 +    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym)
    1.16  
    1.17      def update_style(text: String): String =
    1.18      {