# HG changeset patch
# User wenzelm
# Date 1553448659 -3600
# Node ID c211db89f916957bc21772bdc56cd35b7491b377
# Parent  1a400b14fd3a7e8c8760825db9fb4fb4263c7c08
tuned;

diff -r 1a400b14fd3a -r c211db89f916 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 =
     {