static token markup, based on outer syntax only;
authorwenzelm
Thu Jun 16 22:05:40 2011 +0200 (2011-06-16)
changeset 43414f0770743b7ec
parent 43413 7a7604573ecd
child 43415 8f7494985093
static token markup, based on outer syntax only;
eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/text_area_painter.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 16 20:12:59 2011 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 16 22:05:40 2011 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    "src/scala_console.scala"
     1.5    "src/session_dockable.scala"
     1.6    "src/text_area_painter.scala"
     1.7 +  "src/token_markup.scala"
     1.8  )
     1.9  
    1.10  declare -a RESOURCES=(
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 16 20:12:59 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Jun 16 22:05:40 2011 +0200
     2.3 @@ -14,44 +14,13 @@
     2.4  
     2.5  import org.gjt.sp.jedit.Buffer
     2.6  import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
     2.7 -import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
     2.8  import org.gjt.sp.jedit.textarea.TextArea
     2.9  
    2.10  import java.awt.font.TextAttribute
    2.11 -import javax.swing.text.Segment;
    2.12  
    2.13  
    2.14  object Document_Model
    2.15  {
    2.16 -  object Token_Markup
    2.17 -  {
    2.18 -    /* extended token styles */
    2.19 -
    2.20 -    private val plain_range: Int = Token.ID_COUNT
    2.21 -    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    2.22 -
    2.23 -    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    2.24 -    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    2.25 -    val hidden: Byte = (3 * plain_range).toByte
    2.26 -
    2.27 -
    2.28 -    /* line context */
    2.29 -
    2.30 -    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
    2.31 -
    2.32 -    class Line_Context(val line: Int, prev: Line_Context)
    2.33 -      extends TokenMarker.LineContext(dummy_rules, prev)
    2.34 -    {
    2.35 -      override def hashCode: Int = line
    2.36 -      override def equals(that: Any): Boolean =
    2.37 -        that match {
    2.38 -          case other: Line_Context => line == other.line
    2.39 -          case _ => false
    2.40 -        }
    2.41 -    }
    2.42 -  }
    2.43 -
    2.44 -
    2.45    /* document model of buffer */
    2.46  
    2.47    private val key = "isabelle.document_model"
    2.48 @@ -160,46 +129,9 @@
    2.49    }
    2.50  
    2.51  
    2.52 -  /* semantic token marker */
    2.53 -
    2.54 -  private val token_marker = new TokenMarker
    2.55 -  {
    2.56 -    override def markTokens(prev: TokenMarker.LineContext,
    2.57 -        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
    2.58 -    {
    2.59 -      Isabelle.swing_buffer_lock(buffer) {
    2.60 -        val snapshot = Document_Model.this.snapshot()
    2.61 -
    2.62 -        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
    2.63 -        val line = if (prev == null) 0 else previous.line + 1
    2.64 -        val context = new Document_Model.Token_Markup.Line_Context(line, previous)
    2.65 -
    2.66 -        val start = buffer.getLineStartOffset(line)
    2.67 -        val stop = start + line_segment.count
    2.68 -
    2.69 -        def handle_token(style: Byte, offset: Text.Offset, length: Int) =
    2.70 -          handler.handleToken(line_segment, style, offset, length, context)
    2.71 +  /* token marker */
    2.72  
    2.73 -        val syntax = session.current_syntax()
    2.74 -        val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
    2.75 -
    2.76 -        var last = start
    2.77 -        for (token <- tokens.iterator) {
    2.78 -          val Text.Range(token_start, token_stop) = token.range
    2.79 -          if (last < token_start)
    2.80 -            handle_token(Token.COMMENT1, last - start, token_start - last)
    2.81 -          handle_token(token.info getOrElse Token.NULL,
    2.82 -            token_start - start, token_stop - token_start)
    2.83 -          last = token_stop
    2.84 -        }
    2.85 -        if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
    2.86 -
    2.87 -        handle_token(Token.END, line_segment.count, 0)
    2.88 -        handler.setLineContext(context)
    2.89 -        context
    2.90 -      }
    2.91 -    }
    2.92 -  }
    2.93 +  private val token_marker = Token_Markup.token_marker(session, buffer)
    2.94  
    2.95  
    2.96    /* activation */
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 20:12:59 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 22:05:40 2011 +0200
     3.3 @@ -386,10 +386,6 @@
     3.4                  val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
     3.5                  if line_cmds.exists(changed)
     3.6                } text_area.invalidateScreenLineRange(line, line)
     3.7 -
     3.8 -              // FIXME danger of deadlock!?
     3.9 -              // FIXME potentially slow!?
    3.10 -              model.buffer.propertiesChanged()
    3.11              }
    3.12            }
    3.13  
     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Jun 16 20:12:59 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Thu Jun 16 22:05:40 2011 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  import java.awt.Color
     4.5  
     4.6  import org.lobobrowser.util.gui.ColorFactory
     4.7 -import org.gjt.sp.jedit.syntax.Token
     4.8 +import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     4.9  
    4.10  
    4.11  object Isabelle_Markup
    4.12 @@ -108,6 +108,14 @@
    4.13      case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    4.14    }
    4.15  
    4.16 +  /* FIXME update
    4.17 +      Markup.ML_SOURCE -> COMMENT3,
    4.18 +      Markup.DOC_SOURCE -> COMMENT3,
    4.19 +      Markup.ANTIQ -> COMMENT4,
    4.20 +      Markup.ML_ANTIQ -> COMMENT4,
    4.21 +      Markup.DOC_ANTIQ -> COMMENT4,
    4.22 +  */
    4.23 +
    4.24    private val foreground_colors: Map[String, Color] =
    4.25      Map(
    4.26        Markup.TCLASS -> get_color("red"),
    4.27 @@ -172,7 +180,7 @@
    4.28  
    4.29    private val command_style: Map[String, Byte] =
    4.30    {
    4.31 -    import Token._
    4.32 +    import JEditToken._
    4.33      Map[String, Byte](
    4.34        Keyword.THY_END -> KEYWORD2,
    4.35        Keyword.THY_SCRIPT -> LABEL,
    4.36 @@ -182,39 +190,30 @@
    4.37      ).withDefaultValue(KEYWORD1)
    4.38    }
    4.39  
    4.40 -  private val token_style: Map[String, Byte] =
    4.41 +  private val token_style: Map[Token.Kind.Value, Byte] =
    4.42    {
    4.43 -    import Token._
    4.44 -    Map[String, Byte](
    4.45 -      // embedded source text
    4.46 -      Markup.ML_SOURCE -> COMMENT3,
    4.47 -      Markup.DOC_SOURCE -> COMMENT3,
    4.48 -      Markup.ANTIQ -> COMMENT4,
    4.49 -      Markup.ML_ANTIQ -> COMMENT4,
    4.50 -      Markup.DOC_ANTIQ -> COMMENT4,
    4.51 -      // outer syntax
    4.52 -      Markup.KEYWORD -> KEYWORD2,
    4.53 -      Markup.OPERATOR -> OPERATOR,
    4.54 -      Markup.COMMAND -> KEYWORD1,
    4.55 -      Markup.IDENT -> NULL,
    4.56 -      Markup.VERBATIM -> COMMENT3,
    4.57 -      Markup.COMMENT -> COMMENT1,
    4.58 -      Markup.CONTROL -> COMMENT3,
    4.59 -      Markup.MALFORMED -> INVALID,
    4.60 -      Markup.STRING -> LITERAL3,
    4.61 -      Markup.ALTSTRING -> LITERAL1
    4.62 +    import JEditToken._
    4.63 +    Map[Token.Kind.Value, Byte](
    4.64 +      Token.Kind.KEYWORD -> KEYWORD2,
    4.65 +      Token.Kind.IDENT -> NULL,
    4.66 +      Token.Kind.LONG_IDENT -> NULL,
    4.67 +      Token.Kind.SYM_IDENT -> NULL,
    4.68 +      Token.Kind.VAR -> NULL,
    4.69 +      Token.Kind.TYPE_IDENT -> NULL,
    4.70 +      Token.Kind.TYPE_VAR -> NULL,
    4.71 +      Token.Kind.NAT -> NULL,
    4.72 +      Token.Kind.FLOAT -> NULL,
    4.73 +      Token.Kind.STRING -> LITERAL3,
    4.74 +      Token.Kind.ALT_STRING -> LITERAL1,
    4.75 +      Token.Kind.VERBATIM -> COMMENT3,
    4.76 +      Token.Kind.SPACE -> NULL,
    4.77 +      Token.Kind.COMMENT -> COMMENT1,
    4.78 +      Token.Kind.UNPARSED -> INVALID
    4.79      ).withDefaultValue(NULL)
    4.80    }
    4.81  
    4.82 -  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
    4.83 -  {
    4.84 -    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
    4.85 -    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
    4.86 -
    4.87 -    case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
    4.88 -    if token_style(kind) != Token.NULL => token_style(kind)
    4.89 -
    4.90 -    case Text.Info(_, XML.Elem(Markup(name, _), _))
    4.91 -    if token_style(name) != Token.NULL => token_style(name)
    4.92 -  }
    4.93 +  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
    4.94 +    if (token.is_command)
    4.95 +      command_style(syntax.keyword_kind(token.content).getOrElse(""))
    4.96 +    else token_style(token.kind)
    4.97  }
     5.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Thu Jun 16 20:12:59 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Thu Jun 16 22:05:40 2011 +0200
     5.3 @@ -231,6 +231,7 @@
     5.4          else {
     5.5            var x1 = x + w
     5.6            for (Text.Info(range, info) <- markup) {
     5.7 +            // FIXME range check!?
     5.8              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
     5.9              gfx.setColor(info.getOrElse(chunk_color))
    5.10              if (range.contains(caret_offset)) {
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jun 16 22:05:40 2011 +0200
     6.3 @@ -0,0 +1,75 @@
     6.4 +/*  Title:      Tools/jEdit/src/token_markup.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Outer syntax token markup.
     6.8 +*/
     6.9 +
    6.10 +package isabelle.jedit
    6.11 +
    6.12 +
    6.13 +import isabelle._
    6.14 +
    6.15 +import org.gjt.sp.jedit.Buffer
    6.16 +import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet}
    6.17 +import javax.swing.text.Segment
    6.18 +
    6.19 +
    6.20 +object Token_Markup
    6.21 +{
    6.22 +  /* extended jEdit syntax styles */
    6.23 +
    6.24 +  private val plain_range: Int = JToken.ID_COUNT
    6.25 +  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    6.26 +
    6.27 +  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    6.28 +  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    6.29 +  val hidden: Byte = (3 * plain_range).toByte
    6.30 +
    6.31 +
    6.32 +  /* token marker */
    6.33 +
    6.34 +  private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
    6.35 +
    6.36 +  private class Line_Context(val context: Scan.Context)
    6.37 +    extends TokenMarker.LineContext(isabelle_rules, null)
    6.38 +  {
    6.39 +    override def hashCode: Int = context.hashCode
    6.40 +    override def equals(that: Any): Boolean =
    6.41 +      that match {
    6.42 +        case other: Line_Context => context == other.context
    6.43 +        case _ => false
    6.44 +      }
    6.45 +  }
    6.46 +
    6.47 +  def token_marker(session: Session, buffer: Buffer): TokenMarker =
    6.48 +    new TokenMarker {
    6.49 +      override def markTokens(context: TokenMarker.LineContext,
    6.50 +          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
    6.51 +      {
    6.52 +        Isabelle.swing_buffer_lock(buffer) {
    6.53 +          val syntax = session.current_syntax()
    6.54 +
    6.55 +          val ctxt =
    6.56 +            context match {
    6.57 +              case c: Line_Context => c.context
    6.58 +              case _ => Scan.Finished
    6.59 +            }
    6.60 +
    6.61 +          val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    6.62 +          val context1 = new Line_Context(ctxt1)
    6.63 +
    6.64 +          var offset = 0
    6.65 +          for (token <- tokens) {
    6.66 +            val style = Isabelle_Markup.token_markup(syntax, token)
    6.67 +            val length = token.source.length
    6.68 +            handler.handleToken(line, style, offset, length, context1)
    6.69 +            offset += length
    6.70 +          }
    6.71 +          handler.handleToken(line, JToken.END, line.count, 0, context1)
    6.72 +          handler.setLineContext(context1)
    6.73 +          context1
    6.74 +        }
    6.75 +      }
    6.76 +    }
    6.77 +}
    6.78 +