# HG changeset patch # User wenzelm # Date 1281044623 -7200 # Node ID 8aaa21db41f3e4549be08540bae2547c355d72a1 # Parent d5d0af46f1ec67c1be085e7fa3baee5729047b91 Document_Model: include token marker here; diff -r d5d0af46f1ec -r 8aaa21db41f3 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Aug 05 22:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu Aug 05 23:43:43 2010 +0200 @@ -15,11 +15,136 @@ import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} -import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle} +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 val full_range: Int = 3 * plain_range + 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 } + + private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = + { + import scala.collection.JavaConversions._ + val script_font = + style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))) + new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font) + } + + def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = + { + val new_styles = new Array[SyntaxStyle](full_range) + for (i <- 0 until plain_range) { + val style = styles(i) + new_styles(i) = style + new_styles(subscript(i.toByte)) = script_style(style, -1) + new_styles(superscript(i.toByte)) = script_style(style, 1) + } + new_styles + } + + + /* line context */ + + private val rule_set = new ParserRuleSet("isabelle", "MAIN") + class LineContext(val line: Int, prev: LineContext) + extends TokenMarker.LineContext(rule_set, prev) + + + /* mapping to jEdit token types */ + // TODO: as properties or CSS style sheet + + val command_style: Map[String, Byte] = + { + import Token._ + Map[String, Byte]( + Keyword.THY_END -> KEYWORD2, + Keyword.THY_SCRIPT -> LABEL, + Keyword.PRF_SCRIPT -> LABEL, + Keyword.PRF_ASM -> KEYWORD3, + Keyword.PRF_ASM_GOAL -> KEYWORD3 + ).withDefaultValue(KEYWORD1) + } + + val token_style: Map[String, Byte] = + { + import Token._ + Map[String, Byte]( + // logical entities + Markup.TCLASS -> NULL, + Markup.TYCON -> NULL, + Markup.FIXED_DECL -> FUNCTION, + Markup.FIXED -> NULL, + Markup.CONST_DECL -> FUNCTION, + Markup.CONST -> NULL, + Markup.FACT_DECL -> FUNCTION, + Markup.FACT -> NULL, + Markup.DYNAMIC_FACT -> LABEL, + Markup.LOCAL_FACT_DECL -> FUNCTION, + Markup.LOCAL_FACT -> NULL, + // inner syntax + Markup.TFREE -> NULL, + Markup.FREE -> NULL, + Markup.TVAR -> NULL, + Markup.SKOLEM -> NULL, + Markup.BOUND -> NULL, + Markup.VAR -> NULL, + Markup.NUM -> DIGIT, + Markup.FLOAT -> DIGIT, + Markup.XNUM -> DIGIT, + Markup.XSTR -> LITERAL4, + Markup.LITERAL -> OPERATOR, + Markup.INNER_COMMENT -> COMMENT1, + Markup.SORT -> NULL, + Markup.TYP -> NULL, + Markup.TERM -> NULL, + Markup.PROP -> NULL, + Markup.ATTRIBUTE -> NULL, + Markup.METHOD -> NULL, + // ML syntax + Markup.ML_KEYWORD -> KEYWORD1, + Markup.ML_DELIMITER -> OPERATOR, + Markup.ML_IDENT -> NULL, + Markup.ML_TVAR -> NULL, + Markup.ML_NUMERAL -> DIGIT, + Markup.ML_CHAR -> LITERAL1, + Markup.ML_STRING -> LITERAL1, + Markup.ML_COMMENT -> COMMENT1, + Markup.ML_MALFORMED -> INVALID, + // 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 + ).withDefaultValue(NULL) + } + } + + /* document model of buffer */ private val key = "isabelle.document_model" @@ -81,6 +206,8 @@ // FIXME proper error handling val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2 + def current_change(): Change = history + def snapshot(): Change.Snapshot = Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) } @@ -117,9 +244,70 @@ } - /* activation */ + /* semantic token marker */ + + private val token_marker = new TokenMarker + { + override def markTokens(prev: TokenMarker.LineContext, + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = + { + val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext] + val line = if (prev == null) 0 else previous.line + 1 + val context = new Document_Model.Token_Markup.LineContext(line, previous) + val start = buffer.getLineStartOffset(line) + val stop = start + line_segment.count + + val snapshot = Document_Model.this.snapshot() + + /* FIXME + for (text_area <- Isabelle.jedit_text_areas(buffer) + if Document_View(text_area).isDefined) + Document_View(text_area).get.set_styles() + */ + + def handle_token(style: Byte, offset: Int, length: Int) = + handler.handleToken(line_segment, style, offset, length, context) - private val token_marker = new Isabelle_Token_Marker(this) + var next_x = start + for { + (command, command_start) <- + snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop)) + markup <- snapshot.document.current_state(command).highlight.flatten + val abs_start = snapshot.convert(command_start + markup.start) + val abs_stop = snapshot.convert(command_start + markup.stop) + if (abs_stop > start) + if (abs_start < stop) + val token_start = (abs_start - start) max 0 + val token_length = + (abs_stop - abs_start) - + ((start - abs_start) max 0) - + ((abs_stop - stop) max 0) + } + { + val token_type = + markup.info match { + case Command.HighlightInfo(Markup.COMMAND, Some(kind)) => + Document_Model.Token_Markup.command_style(kind) + case Command.HighlightInfo(kind, _) => + Document_Model.Token_Markup.token_style(kind) + case _ => Token.NULL + } + if (start + token_start > next_x) + handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x) + handle_token(token_type, token_start, token_length) + next_x = start + token_start + token_length + } + if (next_x < stop) + handle_token(Token.COMMENT1, next_x - start, stop - next_x) + + handle_token(Token.END, line_segment.count, 0) + handler.setLineContext(context) + context + } + } + + + /* activation */ def activate() { diff -r d5d0af46f1ec -r 8aaa21db41f3 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 22:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 23:43:43 2010 +0200 @@ -87,7 +87,7 @@ def extend_styles() { Swing_Thread.assert() - styles = Isabelle_Token_Marker.extend_styles(text_area.getPainter.getStyles) + styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles) } extend_styles() diff -r d5d0af46f1ec -r 8aaa21db41f3 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 22:01:25 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,201 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/isabelle_token_marker.scala - Author: Fabian Immler, TU Munich - -Include isabelle's command- and keyword-declarations live in jEdits -syntax-highlighting. -*/ - -package isabelle.jedit - - -import isabelle._ - -import org.gjt.sp.jedit.buffer.JEditBuffer -import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet, SyntaxStyle} -import org.gjt.sp.jedit.textarea.TextArea - -import java.awt.Font -import java.awt.font.TextAttribute -import javax.swing.text.Segment; - - -object Isabelle_Token_Marker -{ - /* extended token styles */ - - private val plain_range: Int = Token.ID_COUNT - private val full_range: Int = 3 * plain_range - 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 } - - private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = - { - import scala.collection.JavaConversions._ - val script_font = - style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))) - new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font) - } - - def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = - { - val new_styles = new Array[SyntaxStyle](full_range) - for (i <- 0 until plain_range) { - val style = styles(i) - new_styles(i) = style - new_styles(subscript(i.toByte)) = script_style(style, -1) - new_styles(superscript(i.toByte)) = script_style(style, 1) - } - new_styles - } - - - /* line context */ - - private val rule_set = new ParserRuleSet("isabelle", "MAIN") - private class LineContext(val line: Int, prev: LineContext) - extends TokenMarker.LineContext(rule_set, prev) - - - /* mapping to jEdit token types */ - // TODO: as properties or CSS style sheet - - private val command_style: Map[String, Byte] = - { - import Token._ - Map[String, Byte]( - Keyword.THY_END -> KEYWORD2, - Keyword.THY_SCRIPT -> LABEL, - Keyword.PRF_SCRIPT -> LABEL, - Keyword.PRF_ASM -> KEYWORD3, - Keyword.PRF_ASM_GOAL -> KEYWORD3 - ).withDefaultValue(KEYWORD1) - } - - private val token_style: Map[String, Byte] = - { - import Token._ - Map[String, Byte]( - // logical entities - Markup.TCLASS -> NULL, - Markup.TYCON -> NULL, - Markup.FIXED_DECL -> FUNCTION, - Markup.FIXED -> NULL, - Markup.CONST_DECL -> FUNCTION, - Markup.CONST -> NULL, - Markup.FACT_DECL -> FUNCTION, - Markup.FACT -> NULL, - Markup.DYNAMIC_FACT -> LABEL, - Markup.LOCAL_FACT_DECL -> FUNCTION, - Markup.LOCAL_FACT -> NULL, - // inner syntax - Markup.TFREE -> NULL, - Markup.FREE -> NULL, - Markup.TVAR -> NULL, - Markup.SKOLEM -> NULL, - Markup.BOUND -> NULL, - Markup.VAR -> NULL, - Markup.NUM -> DIGIT, - Markup.FLOAT -> DIGIT, - Markup.XNUM -> DIGIT, - Markup.XSTR -> LITERAL4, - Markup.LITERAL -> OPERATOR, - Markup.INNER_COMMENT -> COMMENT1, - Markup.SORT -> NULL, - Markup.TYP -> NULL, - Markup.TERM -> NULL, - Markup.PROP -> NULL, - Markup.ATTRIBUTE -> NULL, - Markup.METHOD -> NULL, - // ML syntax - Markup.ML_KEYWORD -> KEYWORD1, - Markup.ML_DELIMITER -> OPERATOR, - Markup.ML_IDENT -> NULL, - Markup.ML_TVAR -> NULL, - Markup.ML_NUMERAL -> DIGIT, - Markup.ML_CHAR -> LITERAL1, - Markup.ML_STRING -> LITERAL1, - Markup.ML_COMMENT -> COMMENT1, - Markup.ML_MALFORMED -> INVALID, - // 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 - ).withDefaultValue(NULL) - } -} - - -class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker -{ - override def markTokens(prev: TokenMarker.LineContext, - handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = - { - val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext] - val line = if (prev == null) 0 else previous.line + 1 - val context = new Isabelle_Token_Marker.LineContext(line, previous) - val start = model.buffer.getLineStartOffset(line) - val stop = start + line_segment.count - - val snapshot = model.snapshot() - - /* FIXME - for (text_area <- Isabelle.jedit_text_areas(model.buffer) - if Document_View(text_area).isDefined) - Document_View(text_area).get.set_styles() - */ - - def handle_token(style: Byte, offset: Int, length: Int) = - handler.handleToken(line_segment, style, offset, length, context) - - var next_x = start - for { - (command, command_start) <- - snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop)) - markup <- snapshot.document.current_state(command).highlight.flatten - val abs_start = snapshot.convert(command_start + markup.start) - val abs_stop = snapshot.convert(command_start + markup.stop) - if (abs_stop > start) - if (abs_start < stop) - val token_start = (abs_start - start) max 0 - val token_length = - (abs_stop - abs_start) - - ((start - abs_start) max 0) - - ((abs_stop - stop) max 0) - } - { - val token_type = - markup.info match { - case Command.HighlightInfo(Markup.COMMAND, Some(kind)) => - Isabelle_Token_Marker.command_style(kind) - case Command.HighlightInfo(kind, _) => - Isabelle_Token_Marker.token_style(kind) - case _ => Token.NULL - } - if (start + token_start > next_x) - handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x) - handle_token(token_type, token_start, token_length) - next_x = start + token_start + token_length - } - if (next_x < stop) - handle_token(Token.COMMENT1, next_x - start, stop - next_x) - - handle_token(Token.END, line_segment.count, 0) - handler.setLineContext(context) - context - } -}