special handling of control symbols in Symbols dockable;
less obscure Scala names;

--- a/src/Tools/jEdit/src/isabelle_actions.scala	Sat Nov 24 16:24:39 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sat Nov 24 16:40:42 2012 +0100
@@ -25,28 +25,28 @@
     }
   }
 
+  def cancel_execution() { Isabelle.session.cancel_execution() }
 
-  def cancel_execution() { Isabelle.session.cancel_execution() }
 
   /* control styles */
 
   def control_sub(text_area: JEditTextArea)
-  { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) }
+  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
 
   def control_sup(text_area: JEditTextArea)
-  { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) }
+  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
 
   def control_isub(text_area: JEditTextArea)
-  { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) }
+  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
 
   def control_isup(text_area: JEditTextArea)
-  { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) }
+  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
 
   def control_bold(text_area: JEditTextArea)
-  { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) }
+  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
 
   def control_reset(text_area: JEditTextArea)
-  { Token_Markup.edit_ctrl_style(text_area, "") }
+  { Token_Markup.edit_control_style(text_area, "") }
 
 
   /* block styles */

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:24:39 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:40:42 2012 +0100
@@ -25,22 +25,42 @@
 
   private class Symbol_Component(val symbol: String) extends Button
   {
-    val dec = Symbol.decode(symbol)
+    private val decoded = Symbol.decode(symbol)
     font =
       new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
-    action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
+    action =
+      Action(decoded) {
+        val text_area = view.getTextArea
+        if (Token_Markup.is_control_style(decoded))
+          Token_Markup.edit_control_style(text_area, decoded)
+        else text_area.setSelectedText(decoded)
+        text_area.requestFocus
+      }
     tooltip =
       JEdit_Lib.wrap_tooltip(
         symbol +
           (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else ""))
   }
 
+  private class Reset_Component extends Button
+  {
+    action = Action("Reset") {
+      val text_area = view.getTextArea
+      Token_Markup.edit_control_style(text_area, "")
+      text_area.requestFocus
+    }
+    tooltip = "Reset control symbols within text"
+  }
+
   val group_tabs: TabbedPane = new TabbedPane {
     pages ++= (for ((group, symbols) <- Symbol.groups) yield
       {
         new TabbedPane.Page(group,
-          new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) })
+          new FlowPanel {
+            contents ++= symbols.map(new Symbol_Component(_))
+            if (group == "control") contents += new Reset_Component
+          })
       }).toList.sortWith(_.title <= _.title)
     pages += new TabbedPane.Page("search", new BorderPanel {
       val search = new TextField(10)

--- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 16:24:39 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 16:40:42 2012 +0100
@@ -27,45 +27,45 @@
 {
   /* editing support for control symbols */
 
-  private val is_ctrl_style =
+  val is_control_style =
     Set(Symbol.sub_decoded, Symbol.sup_decoded,
       Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
 
-  def update_ctrl_style(ctrl: String, text: String): String =
+  def update_control_style(control: String, text: String): String =
   {
     val result = new StringBuilder
-    for (sym <- Symbol.iterator(text) if !is_ctrl_style(sym)) {
-      if (Symbol.is_controllable(sym)) result ++= ctrl
+    for (sym <- Symbol.iterator(text) if !is_control_style(sym)) {
+      if (Symbol.is_controllable(sym)) result ++= control
       result ++= sym
     }
     result.toString
   }
 
-  def edit_ctrl_style(text_area: TextArea, ctrl: String)
+  def edit_control_style(text_area: TextArea, control: String)
   {
     Swing_Thread.assert()
 
     val buffer = text_area.getBuffer
 
     text_area.getSelection.toList match {
-      case Nil if ctrl == "" =>
+      case Nil if control == "" =>
         try {
           buffer.beginCompoundEdit()
           val caret = text_area.getCaretPosition
-          if (caret > 0 && is_ctrl_style(buffer.getText(caret - 1, 1)))
+          if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
             text_area.backspace()
         }
         finally {
           buffer.endCompoundEdit()
         }
-      case Nil if ctrl != "" =>
-        text_area.setSelectedText(ctrl)
+      case Nil if control != "" =>
+        text_area.setSelectedText(control)
       case sels =>
         try {
           buffer.beginCompoundEdit()
           sels.foreach(sel =>
             text_area.setSelectedText(sel,
-              update_ctrl_style(ctrl, text_area.getSelectedText(sel))))
+              update_control_style(control, text_area.getSelectedText(sel))))
         }
         finally {
           buffer.endCompoundEdit()
@@ -165,7 +165,7 @@
   def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
     // FIXME Symbol.bsub_decoded etc.
-    def ctrl_style(sym: String): Option[Byte => Byte] =
+    def control_style(sym: String): Option[Byte => Byte] =
       if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
       else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
       else if (sym == Symbol.bold_decoded) Some(bold(_))
@@ -177,15 +177,15 @@
       for (i <- start until stop) result += (i -> style)
     }
     var offset = 0
-    var ctrl = ""
+    var control = ""
     for (sym <- Symbol.iterator(text)) {
-      if (ctrl_style(sym).isDefined) ctrl = sym
-      else if (ctrl != "") {
+      if (control_style(sym).isDefined) control = sym
+      else if (control != "") {
         if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
-          mark(offset - ctrl.length, offset, _ => hidden)
-          mark(offset, offset + sym.length, ctrl_style(ctrl).get)
+          mark(offset - control.length, offset, _ => hidden)
+          mark(offset, offset + sym.length, control_style(control).get)
         }
-        ctrl = ""
+        control = ""
       }
       Symbol.lookup_font(sym) match {
         case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))