tuned;
authorwenzelm
Sun, 24 Mar 2019 18:30:59 +0100
changeset 69969 c211db89f916
parent 69968 1a400b14fd3a
child 69970 b5a47478897a
tuned;
src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Sun Mar 24 17:53:46 2019 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Sun Mar 24 18:30:59 2019 +0100
@@ -148,13 +148,13 @@
 
   /* editing support for control symbols */
 
-  def edit_control_style(text_area: TextArea, control: String)
+  def edit_control_style(text_area: TextArea, control_sym: String)
   {
     GUI_Thread.assert {}
 
     val buffer = text_area.getBuffer
 
-    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
+    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym)
 
     def update_style(text: String): String =
     {