basic support for extended syntax styles: sub/superscript;

--- a/src/Pure/General/symbol.scala	Sat Jun 18 17:32:13 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sat Jun 18 17:33:27 2011 +0200
@@ -326,5 +326,7 @@
     def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
     def is_symbolic(sym: String): Boolean =
       sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
+    def is_controllable(sym: String): Boolean =
+      !is_blank(sym) && !sym.startsWith("\\<^")
   }
 }

--- a/src/Pure/System/session.scala	Sat Jun 18 17:32:13 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jun 18 17:33:27 2011 +0200
@@ -31,7 +31,7 @@
 }
 
 
-class Session(system: Isabelle_System)
+class Session(val system: Isabelle_System)
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 

--- a/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 17:32:13 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 17:33:27 2011 +0200
@@ -19,9 +19,11 @@
   Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.syntax.{Token => JEditToken}
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
+import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.util.Log
 
 import scala.actors.Actor
@@ -32,10 +34,16 @@
 {
   /* plugin instance */
 
+  var plugin: Plugin = null
   var system: Isabelle_System = null
   var session: Session = null
 
 
+  /* extended syntax styles */
+
+  def extended_styles: Boolean = plugin != null && plugin._extended_styles
+
+
   /* properties */
 
   val OPTION_PREFIX = "options.isabelle."
@@ -256,6 +264,19 @@
 
 class Plugin extends EBPlugin
 {
+  /* extended syntax styles */
+
+  @volatile var _extended_styles: Boolean = false
+
+  private def check_extended_styles()
+  {
+    val family = jEdit.getProperty("view.font")
+    val size = jEdit.getIntegerProperty("view.fontsize", 12)
+    val styles = SyntaxUtilities.loadStyles(family, size)
+    _extended_styles = (styles.length == JEditToken.ID_COUNT * 3 + 1)
+  }
+
+
   /* session management */
 
   private def init_model(buffer: Buffer)
@@ -346,6 +367,7 @@
     message match {
       case msg: EditorStarted =>
       Isabelle.check_jvm()
+      check_extended_styles()
       if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
 
       case msg: BufferUpdate
@@ -382,6 +404,7 @@
 
   override def start()
   {
+    Isabelle.plugin = this
     Isabelle.setup_tooltips()
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()

--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 17:32:13 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 17:33:27 2011 +0200
@@ -16,7 +16,7 @@
 
 object Token_Markup
 {
-  /* extended jEdit syntax styles */
+  /* extended syntax styles */
 
   private val plain_range: Int = JEditToken.ID_COUNT
   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
@@ -25,6 +25,43 @@
   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
   val hidden: Byte = (3 * plain_range).toByte
 
+  // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
+  // FIXME \\<^bold> \\<^loc>
+
+  private val ctrl_styles: Map[String, Byte => Byte] =
+    Map(
+      "\\<^sub>" -> subscript,
+      "\\<^sup>" -> superscript,
+      "\\<^isub>" -> subscript,
+      "\\<^isup>" -> superscript)
+
+  private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
+    : Map[Text.Offset, Byte => Byte] =
+  {
+    if (Isabelle.extended_styles) {
+      var result = Map[Text.Offset, Byte => Byte]()
+      def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
+      {
+        for (i <- start until stop) result += (i -> style)
+      }
+      var offset = 0
+      var ctrl = ""
+      for (sym <- Symbol.iterator(text).map(_.toString)) {
+        if (ctrl_styles.isDefinedAt(sym)) ctrl = sym
+        else if (ctrl != "") {
+          if (symbols.is_controllable(sym)) {
+            mark(offset - ctrl.length, offset, _ => hidden)
+            mark(offset, offset + sym.length, ctrl_styles(ctrl))
+          }
+          ctrl = ""
+        }
+        offset += sym.length
+      }
+      result
+    }
+    else Map.empty
+  }
+
 
   /* token marker */
 
@@ -55,11 +92,24 @@
         val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
         val context1 = new Line_Context(ctxt1)
 
+        val extended = extended_styles(session.system.symbols, line)
+
         var offset = 0
         for (token <- tokens) {
           val style = Isabelle_Markup.token_markup(syntax, token)
           val length = token.source.length
-          handler.handleToken(line, style, offset, length, context1)
+          val end_offset = offset + length
+          if ((offset until end_offset) exists extended.isDefinedAt) {
+            for (i <- offset until end_offset) {
+              val style1 =
+                extended.get(i) match {
+                  case None => style
+                  case Some(ext) => ext(style)
+                }
+              handler.handleToken(line, style1, i, 1, context1)
+            }
+          }
+          else handler.handleToken(line, style, offset, length, context1)
           offset += length
         }
         handler.handleToken(line, JEditToken.END, line.count, 0, context1)