# HG changeset patch # User wenzelm # Date 1308254740 -7200 # Node ID f0770743b7ecff1cefa5f5adc5504af594bed4ce # Parent 7a7604573ecd2f5431e35d46d2b7ebbdb40f5649 static token markup, based on outer syntax only; eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.); diff -r 7a7604573ecd -r f0770743b7ec src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Jun 16 20:12:59 2011 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jun 16 22:05:40 2011 +0200 @@ -24,6 +24,7 @@ "src/scala_console.scala" "src/session_dockable.scala" "src/text_area_painter.scala" + "src/token_markup.scala" ) declare -a RESOURCES=( diff -r 7a7604573ecd -r f0770743b7ec src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Jun 16 20:12:59 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Thu Jun 16 22:05:40 2011 +0200 @@ -14,44 +14,13 @@ import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} -import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet} import org.gjt.sp.jedit.textarea.TextArea import java.awt.font.TextAttribute -import javax.swing.text.Segment; object Document_Model { - object Token_Markup - { - /* extended token styles */ - - private val plain_range: Int = Token.ID_COUNT - private def check_range(i: Int) { require(0 <= i && i < plain_range) } - - def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } - def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } - val hidden: Byte = (3 * plain_range).toByte - - - /* line context */ - - private val dummy_rules = new ParserRuleSet("isabelle", "MAIN") - - class Line_Context(val line: Int, prev: Line_Context) - extends TokenMarker.LineContext(dummy_rules, prev) - { - override def hashCode: Int = line - override def equals(that: Any): Boolean = - that match { - case other: Line_Context => line == other.line - case _ => false - } - } - } - - /* document model of buffer */ private val key = "isabelle.document_model" @@ -160,46 +129,9 @@ } - /* semantic token marker */ - - private val token_marker = new TokenMarker - { - override def markTokens(prev: TokenMarker.LineContext, - handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = - { - Isabelle.swing_buffer_lock(buffer) { - val snapshot = Document_Model.this.snapshot() - - val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context] - val line = if (prev == null) 0 else previous.line + 1 - val context = new Document_Model.Token_Markup.Line_Context(line, previous) - - val start = buffer.getLineStartOffset(line) - val stop = start + line_segment.count - - def handle_token(style: Byte, offset: Text.Offset, length: Int) = - handler.handleToken(line_segment, style, offset, length, context) + /* token marker */ - val syntax = session.current_syntax() - val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax)) - - var last = start - for (token <- tokens.iterator) { - val Text.Range(token_start, token_stop) = token.range - if (last < token_start) - handle_token(Token.COMMENT1, last - start, token_start - last) - handle_token(token.info getOrElse Token.NULL, - token_start - start, token_stop - token_start) - last = token_stop - } - if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last) - - handle_token(Token.END, line_segment.count, 0) - handler.setLineContext(context) - context - } - } - } + private val token_marker = Token_Markup.token_marker(session, buffer) /* activation */ diff -r 7a7604573ecd -r f0770743b7ec src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Jun 16 20:12:59 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Thu Jun 16 22:05:40 2011 +0200 @@ -386,10 +386,6 @@ val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) if line_cmds.exists(changed) } text_area.invalidateScreenLineRange(line, line) - - // FIXME danger of deadlock!? - // FIXME potentially slow!? - model.buffer.propertiesChanged() } } diff -r 7a7604573ecd -r f0770743b7ec src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Thu Jun 16 20:12:59 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Thu Jun 16 22:05:40 2011 +0200 @@ -12,7 +12,7 @@ import java.awt.Color import org.lobobrowser.util.gui.ColorFactory -import org.gjt.sp.jedit.syntax.Token +import org.gjt.sp.jedit.syntax.{Token => JEditToken} object Isabelle_Markup @@ -108,6 +108,14 @@ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color } + /* FIXME update + Markup.ML_SOURCE -> COMMENT3, + Markup.DOC_SOURCE -> COMMENT3, + Markup.ANTIQ -> COMMENT4, + Markup.ML_ANTIQ -> COMMENT4, + Markup.DOC_ANTIQ -> COMMENT4, + */ + private val foreground_colors: Map[String, Color] = Map( Markup.TCLASS -> get_color("red"), @@ -172,7 +180,7 @@ private val command_style: Map[String, Byte] = { - import Token._ + import JEditToken._ Map[String, Byte]( Keyword.THY_END -> KEYWORD2, Keyword.THY_SCRIPT -> LABEL, @@ -182,39 +190,30 @@ ).withDefaultValue(KEYWORD1) } - private val token_style: Map[String, Byte] = + private val token_style: Map[Token.Kind.Value, Byte] = { - import Token._ - Map[String, Byte]( - // embedded source text - Markup.ML_SOURCE -> COMMENT3, - Markup.DOC_SOURCE -> COMMENT3, - Markup.ANTIQ -> COMMENT4, - Markup.ML_ANTIQ -> COMMENT4, - Markup.DOC_ANTIQ -> COMMENT4, - // outer syntax - Markup.KEYWORD -> KEYWORD2, - Markup.OPERATOR -> OPERATOR, - Markup.COMMAND -> KEYWORD1, - Markup.IDENT -> NULL, - Markup.VERBATIM -> COMMENT3, - Markup.COMMENT -> COMMENT1, - Markup.CONTROL -> COMMENT3, - Markup.MALFORMED -> INVALID, - Markup.STRING -> LITERAL3, - Markup.ALTSTRING -> LITERAL1 + import JEditToken._ + Map[Token.Kind.Value, Byte]( + Token.Kind.KEYWORD -> KEYWORD2, + Token.Kind.IDENT -> NULL, + Token.Kind.LONG_IDENT -> NULL, + Token.Kind.SYM_IDENT -> NULL, + Token.Kind.VAR -> NULL, + Token.Kind.TYPE_IDENT -> NULL, + Token.Kind.TYPE_VAR -> NULL, + Token.Kind.NAT -> NULL, + Token.Kind.FLOAT -> NULL, + Token.Kind.STRING -> LITERAL3, + Token.Kind.ALT_STRING -> LITERAL1, + Token.Kind.VERBATIM -> COMMENT3, + Token.Kind.SPACE -> NULL, + Token.Kind.COMMENT -> COMMENT1, + Token.Kind.UNPARSED -> INVALID ).withDefaultValue(NULL) } - def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] = - { - case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) - if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get) - - case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _)) - if token_style(kind) != Token.NULL => token_style(kind) - - case Text.Info(_, XML.Elem(Markup(name, _), _)) - if token_style(name) != Token.NULL => token_style(name) - } + def token_markup(syntax: Outer_Syntax, token: Token): Byte = + if (token.is_command) + command_style(syntax.keyword_kind(token.content).getOrElse("")) + else token_style(token.kind) } diff -r 7a7604573ecd -r f0770743b7ec src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Thu Jun 16 20:12:59 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Thu Jun 16 22:05:40 2011 +0200 @@ -231,6 +231,7 @@ else { var x1 = x + w for (Text.Info(range, info) <- markup) { + // FIXME range check!? val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) gfx.setColor(info.getOrElse(chunk_color)) if (range.contains(caret_offset)) { diff -r 7a7604573ecd -r f0770743b7ec src/Tools/jEdit/src/token_markup.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/token_markup.scala Thu Jun 16 22:05:40 2011 +0200 @@ -0,0 +1,75 @@ +/* Title: Tools/jEdit/src/token_markup.scala + Author: Makarius + +Outer syntax token markup. +*/ + +package isabelle.jedit + + +import isabelle._ + +import org.gjt.sp.jedit.Buffer +import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet} +import javax.swing.text.Segment + + +object Token_Markup +{ + /* extended jEdit syntax styles */ + + private val plain_range: Int = JToken.ID_COUNT + private def check_range(i: Int) { require(0 <= i && i < plain_range) } + + def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } + def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } + val hidden: Byte = (3 * plain_range).toByte + + + /* token marker */ + + private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN") + + private class Line_Context(val context: Scan.Context) + extends TokenMarker.LineContext(isabelle_rules, null) + { + override def hashCode: Int = context.hashCode + override def equals(that: Any): Boolean = + that match { + case other: Line_Context => context == other.context + case _ => false + } + } + + def token_marker(session: Session, buffer: Buffer): TokenMarker = + new TokenMarker { + override def markTokens(context: TokenMarker.LineContext, + handler: TokenHandler, line: Segment): TokenMarker.LineContext = + { + Isabelle.swing_buffer_lock(buffer) { + val syntax = session.current_syntax() + + val ctxt = + context match { + case c: Line_Context => c.context + case _ => Scan.Finished + } + + val (tokens, ctxt1) = syntax.scan_context(line, ctxt) + val context1 = new Line_Context(ctxt1) + + 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) + offset += length + } + handler.handleToken(line, JToken.END, line.count, 0, context1) + handler.setLineContext(context1) + context1 + } + } + } +} +