1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jun 16 22:05:40 2011 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +/*  Title:      Tools/jEdit/src/token_markup.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Outer syntax token markup.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import org.gjt.sp.jedit.Buffer
    1.16 +import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet}
    1.17 +import javax.swing.text.Segment
    1.18 +
    1.19 +
    1.20 +object Token_Markup
    1.21 +{
    1.22 +  /* extended jEdit syntax styles */
    1.23 +
    1.24 +  private val plain_range: Int = JToken.ID_COUNT
    1.25 +  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    1.26 +
    1.27 +  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    1.28 +  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    1.29 +  val hidden: Byte = (3 * plain_range).toByte
    1.30 +
    1.31 +
    1.32 +  /* token marker */
    1.33 +
    1.34 +  private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
    1.35 +
    1.36 +  private class Line_Context(val context: Scan.Context)
    1.37 +    extends TokenMarker.LineContext(isabelle_rules, null)
    1.38 +  {
    1.39 +    override def hashCode: Int = context.hashCode
    1.40 +    override def equals(that: Any): Boolean =
    1.41 +      that match {
    1.42 +        case other: Line_Context => context == other.context
    1.43 +        case _ => false
    1.44 +      }
    1.45 +  }
    1.46 +
    1.47 +  def token_marker(session: Session, buffer: Buffer): TokenMarker =
    1.48 +    new TokenMarker {
    1.49 +      override def markTokens(context: TokenMarker.LineContext,
    1.50 +          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
    1.51 +      {
    1.52 +        Isabelle.swing_buffer_lock(buffer) {
    1.53 +          val syntax = session.current_syntax()
    1.54 +
    1.55 +          val ctxt =
    1.56 +            context match {
    1.57 +              case c: Line_Context => c.context
    1.58 +              case _ => Scan.Finished
    1.59 +            }
    1.60 +
    1.61 +          val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    1.62 +          val context1 = new Line_Context(ctxt1)
    1.63 +
    1.64 +          var offset = 0
    1.65 +          for (token <- tokens) {
    1.66 +            val style = Isabelle_Markup.token_markup(syntax, token)
    1.67 +            val length = token.source.length
    1.68 +            handler.handleToken(line, style, offset, length, context1)
    1.69 +            offset += length
    1.70 +          }
    1.71 +          handler.handleToken(line, JToken.END, line.count, 0, context1)
    1.72 +          handler.setLineContext(context1)
    1.73 +          context1
    1.74 +        }
    1.75 +      }
    1.76 +    }
    1.77 +}
    1.78 +