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

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

     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 17:32:13 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 17:33:27 2011 +0200
     3.3 @@ -19,9 +19,11 @@
     3.4    Buffer, EditPane, ServiceManager, View}
     3.5  import org.gjt.sp.jedit.buffer.JEditBuffer
     3.6  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     3.7 +import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     3.8  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     3.9  import org.gjt.sp.jedit.gui.DockableWindowManager
    3.10  
    3.11 +import org.gjt.sp.util.SyntaxUtilities
    3.12  import org.gjt.sp.util.Log
    3.13  
    3.14  import scala.actors.Actor
    3.15 @@ -32,10 +34,16 @@
    3.16  {
    3.17    /* plugin instance */
    3.18  
    3.19 +  var plugin: Plugin = null
    3.20    var system: Isabelle_System = null
    3.21    var session: Session = null
    3.22  
    3.23  
    3.24 +  /* extended syntax styles */
    3.25 +
    3.26 +  def extended_styles: Boolean = plugin != null && plugin._extended_styles
    3.27 +
    3.28 +
    3.29    /* properties */
    3.30  
    3.31    val OPTION_PREFIX = "options.isabelle."
    3.32 @@ -256,6 +264,19 @@
    3.33  
    3.34  class Plugin extends EBPlugin
    3.35  {
    3.36 +  /* extended syntax styles */
    3.37 +
    3.38 +  @volatile var _extended_styles: Boolean = false
    3.39 +
    3.40 +  private def check_extended_styles()
    3.41 +  {
    3.42 +    val family = jEdit.getProperty("view.font")
    3.43 +    val size = jEdit.getIntegerProperty("view.fontsize", 12)
    3.44 +    val styles = SyntaxUtilities.loadStyles(family, size)
    3.45 +    _extended_styles = (styles.length == JEditToken.ID_COUNT * 3 + 1)
    3.46 +  }
    3.47 +
    3.48 +
    3.49    /* session management */
    3.50  
    3.51    private def init_model(buffer: Buffer)
    3.52 @@ -346,6 +367,7 @@
    3.53      message match {
    3.54        case msg: EditorStarted =>
    3.55        Isabelle.check_jvm()
    3.56 +      check_extended_styles()
    3.57        if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
    3.58  
    3.59        case msg: BufferUpdate
    3.60 @@ -382,6 +404,7 @@
    3.61  
    3.62    override def start()
    3.63    {
    3.64 +    Isabelle.plugin = this
    3.65      Isabelle.setup_tooltips()
    3.66      Isabelle.system = new Isabelle_System
    3.67      Isabelle.system.install_fonts()

     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 17:32:13 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 17:33:27 2011 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4  
     4.5  object Token_Markup
     4.6  {
     4.7 -  /* extended jEdit syntax styles */
     4.8 +  /* extended syntax styles */
     4.9  
    4.10    private val plain_range: Int = JEditToken.ID_COUNT
    4.11    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    4.12 @@ -25,6 +25,43 @@
    4.13    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    4.14    val hidden: Byte = (3 * plain_range).toByte
    4.15  
    4.16 +  // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
    4.17 +  // FIXME \\<^bold> \\<^loc>
    4.18 +
    4.19 +  private val ctrl_styles: Map[String, Byte => Byte] =
    4.20 +    Map(
    4.21 +      "\\<^sub>" -> subscript,
    4.22 +      "\\<^sup>" -> superscript,
    4.23 +      "\\<^isub>" -> subscript,
    4.24 +      "\\<^isup>" -> superscript)
    4.25 +
    4.26 +  private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
    4.27 +    : Map[Text.Offset, Byte => Byte] =
    4.28 +  {
    4.29 +    if (Isabelle.extended_styles) {
    4.30 +      var result = Map[Text.Offset, Byte => Byte]()
    4.31 +      def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
    4.32 +      {
    4.33 +        for (i <- start until stop) result += (i -> style)
    4.34 +      }
    4.35 +      var offset = 0
    4.36 +      var ctrl = ""
    4.37 +      for (sym <- Symbol.iterator(text).map(_.toString)) {
    4.38 +        if (ctrl_styles.isDefinedAt(sym)) ctrl = sym
    4.39 +        else if (ctrl != "") {
    4.40 +          if (symbols.is_controllable(sym)) {
    4.41 +            mark(offset - ctrl.length, offset, _ => hidden)
    4.42 +            mark(offset, offset + sym.length, ctrl_styles(ctrl))
    4.43 +          }
    4.44 +          ctrl = ""
    4.45 +        }
    4.46 +        offset += sym.length
    4.47 +      }
    4.48 +      result
    4.49 +    }
    4.50 +    else Map.empty
    4.51 +  }
    4.52 +
    4.53  
    4.54    /* token marker */
    4.55  
    4.56 @@ -55,11 +92,24 @@
    4.57          val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    4.58          val context1 = new Line_Context(ctxt1)
    4.59  
    4.60 +        val extended = extended_styles(session.system.symbols, line)
    4.61 +
    4.62          var offset = 0
    4.63          for (token <- tokens) {
    4.64            val style = Isabelle_Markup.token_markup(syntax, token)
    4.65            val length = token.source.length
    4.66 -          handler.handleToken(line, style, offset, length, context1)
    4.67 +          val end_offset = offset + length
    4.68 +          if ((offset until end_offset) exists extended.isDefinedAt) {
    4.69 +            for (i <- offset until end_offset) {
    4.70 +              val style1 =
    4.71 +                extended.get(i) match {
    4.72 +                  case None => style
    4.73 +                  case Some(ext) => ext(style)
    4.74 +                }
    4.75 +              handler.handleToken(line, style1, i, 1, context1)
    4.76 +            }
    4.77 +          }
    4.78 +          else handler.handleToken(line, style, offset, length, context1)
    4.79            offset += length
    4.80          }
    4.81          handler.handleToken(line, JEditToken.END, line.count, 0, context1)