some convenience actions/shortcuts for control symbols;

--- a/src/Pure/General/symbol.scala	Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Pure/General/symbol.scala	Wed Aug 17 16:01:27 2011 +0200
@@ -356,14 +356,15 @@
     val ctrl_decoded: Set[Symbol] =
       Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
 
-    val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
-    val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
-
-    val bold_decoded = decode("\\<^bold>")
+    val sub_decoded = decode("\\<^sub>")
+    val sup_decoded = decode("\\<^sup>")
+    val isub_decoded = decode("\\<^isub>")
+    val isup_decoded = decode("\\<^isup>")
     val bsub_decoded = decode("\\<^bsub>")
     val esub_decoded = decode("\\<^esub>")
     val bsup_decoded = decode("\\<^bsup>")
     val esup_decoded = decode("\\<^esup>")
+    val bold_decoded = decode("\\<^bold>")
   }
 
 
@@ -401,11 +402,13 @@
   def is_controllable(sym: Symbol): Boolean =
     !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
 
-  def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
-  def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
-  def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
-  def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
-  def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
-  def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
-  def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
+  def sub_decoded: Symbol = symbols.sub_decoded
+  def sup_decoded: Symbol = symbols.sup_decoded
+  def isub_decoded: Symbol = symbols.isub_decoded
+  def isup_decoded: Symbol = symbols.isup_decoded
+  def bsub_decoded: Symbol = symbols.bsub_decoded
+  def esub_decoded: Symbol = symbols.esub_decoded
+  def bsup_decoded: Symbol = symbols.bsup_decoded
+  def esup_decoded: Symbol = symbols.esup_decoded
+  def bold_decoded: Symbol = symbols.bold_decoded
 }

--- a/src/Pure/Thy/html.scala	Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Pure/Thy/html.scala	Wed Aug 17 16:01:27 2011 +0200
@@ -83,13 +83,15 @@
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""
             if (s1 == "\n") add(XML.elem(BR))
-            else if (Symbol.is_bsub_decoded(s1)) t ++= s1  // FIXME
-            else if (Symbol.is_esub_decoded(s1)) t ++= s1  // FIXME
-            else if (Symbol.is_bsup_decoded(s1)) t ++= s1  // FIXME
-            else if (Symbol.is_esup_decoded(s1)) t ++= s1  // FIXME
-            else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
-            else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
-            else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+            else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
+              { add(hidden(s1)); add(sub(s2())) }
+            else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
+              { add(hidden(s1)); add(sup(s2())) }
+            else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME
+            else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME
+            else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME
+            else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME
+            else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
             else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
             else t ++= s1
           }

--- a/src/Tools/jEdit/src/Isabelle.props	Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Wed Aug 17 16:01:27 2011 +0200
@@ -37,6 +37,11 @@
 options.isabelle.auto-start.title=Auto Start
 options.isabelle.auto-start=true
 
+#actions
+isabelle.input-isub.shortcut=C+e DOWN
+isabelle.input-isup.shortcut=C+e UP
+isabelle.input-bold.shortcut=C+e RIGHT
+
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel

--- a/src/Tools/jEdit/src/actions.xml	Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Wed Aug 17 16:01:27 2011 +0200
@@ -22,4 +22,40 @@
 			wm.addDockableWindow("isabelle-protocol");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.input-sub">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_sub(textArea);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.input-sup">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_sup(textArea);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.input-isub">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_isub(textArea);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.input-isup">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_isup(textArea);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.input-bsub">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_bsub(textArea);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.input-bsup">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_bsup(textArea);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.input-bold">
+	  <CODE>
+	    isabelle.jedit.Isabelle.input_bold(textArea);
+	  </CODE>
+	</ACTION>
+
 </ACTIONS>
\ No newline at end of file

--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 17 16:01:27 2011 +0200
@@ -316,6 +316,24 @@
     }
     session.start(timeout, modes ::: List(logic))
   }
+
+
+  /* convenience actions */
+
+  private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
+  {
+    s1.foreach(text_area.userInput(_))
+    s2.foreach(text_area.userInput(_))
+    s2.foreach(_ => text_area.goToPrevCharacter(false))
+  }
+
+  def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
+  def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
+  def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
+  def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
+  def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
+  def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
+  def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
 }
 
 

--- a/src/Tools/jEdit/src/token_markup.scala	Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Aug 17 16:01:27 2011 +0200
@@ -107,11 +107,11 @@
 
   def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
-    // FIXME Symbol.is_bsub_decoded etc.
+    // FIXME Symbol.bsub_decoded etc.
     def ctrl_style(sym: String): Option[Byte => Byte] =
-      if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
-      else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
-      else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
+      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(_))
       else None
 
     var result = Map[Text.Offset, Byte => Byte]()