src/Tools/jEdit/src/token_markup.scala
author wenzelm
Thu Jun 16 22:05:40 2011 +0200 (2011-06-16)
changeset 43414 f0770743b7ec
child 43416 e730cdd97dcf
permissions -rw-r--r--
static token markup, based on outer syntax only;
eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);
     1 /*  Title:      Tools/jEdit/src/token_markup.scala
     2     Author:     Makarius
     3 
     4 Outer syntax token markup.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.Buffer
    13 import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet}
    14 import javax.swing.text.Segment
    15 
    16 
    17 object Token_Markup
    18 {
    19   /* extended jEdit syntax styles */
    20 
    21   private val plain_range: Int = JToken.ID_COUNT
    22   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    23 
    24   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    25   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    26   val hidden: Byte = (3 * plain_range).toByte
    27 
    28 
    29   /* token marker */
    30 
    31   private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
    32 
    33   private class Line_Context(val context: Scan.Context)
    34     extends TokenMarker.LineContext(isabelle_rules, null)
    35   {
    36     override def hashCode: Int = context.hashCode
    37     override def equals(that: Any): Boolean =
    38       that match {
    39         case other: Line_Context => context == other.context
    40         case _ => false
    41       }
    42   }
    43 
    44   def token_marker(session: Session, buffer: Buffer): TokenMarker =
    45     new TokenMarker {
    46       override def markTokens(context: TokenMarker.LineContext,
    47           handler: TokenHandler, line: Segment): TokenMarker.LineContext =
    48       {
    49         Isabelle.swing_buffer_lock(buffer) {
    50           val syntax = session.current_syntax()
    51 
    52           val ctxt =
    53             context match {
    54               case c: Line_Context => c.context
    55               case _ => Scan.Finished
    56             }
    57 
    58           val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    59           val context1 = new Line_Context(ctxt1)
    60 
    61           var offset = 0
    62           for (token <- tokens) {
    63             val style = Isabelle_Markup.token_markup(syntax, token)
    64             val length = token.source.length
    65             handler.handleToken(line, style, offset, length, context1)
    66             offset += length
    67           }
    68           handler.handleToken(line, JToken.END, line.count, 0, context1)
    69           handler.setLineContext(context1)
    70           context1
    71         }
    72       }
    73     }
    74 }
    75