# HG changeset patch # User immler@in.tum.de # Date 1233612325 -3600 # Node ID 163cda24961990b1347c090e58ffb7b378e60630 # Parent 73225f520f8cededd4396ea2232bd3a1ac9ade15 implemented markTokens; moved choose_color to DynamicTokenMarker and extended to choose_style diff -r 73225f520f8c -r 163cda249619 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Feb 01 13:57:59 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Feb 02 23:05:25 2009 +0100 @@ -1,7 +1,7 @@ /* * include isabelle's command- and keyword-declarations * live in jEdits syntax-highlighting - * + * * one TokenMarker per prover * * @author Fabian Immler, TU Munich @@ -9,42 +9,115 @@ package isabelle.jedit -import org.gjt.sp.jedit.syntax.{ModeProvider, Token, TokenMarker, ParserRuleSet, KeywordMap} +import isabelle.proofdocument.ProofDocument +import isabelle.prover.{Command, MarkupNode} +import isabelle.Markup -class DynamicTokenMarker extends TokenMarker { +import org.gjt.sp.jedit.buffer.JEditBuffer +import org.gjt.sp.jedit.syntax._ - val ruleset = new ParserRuleSet("isabelle", "MAIN") +import java.awt.Color +import java.awt.Font +import javax.swing.text.Segment; + +object DynamicTokenMarker { - // copy rules and keywords from basic isabelle mode - val original = ModeProvider.instance.getMode("isabelle").getTokenMarker.getMainRuleSet - ruleset.addRuleSet(original) - ruleset.setKeywords(new KeywordMap(false)) - ruleset.setDefault(0) - ruleset.setDigitRegexp(null) - ruleset.setEscapeRule(original.getEscapeRule) - ruleset.setHighlightDigits(false) - ruleset.setIgnoreCase(false) - ruleset.setNoWordSep("_'.?") - ruleset.setProperties(null) - ruleset.setTerminateChar(-1) - - addRuleSet(ruleset) + def styles: Array[SyntaxStyle] = { + val array = new Array[SyntaxStyle](256) + // array(0) won't be used: reserved for global default-font + array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font) + array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font) + array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font) + array(4) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font) + array(5) = new SyntaxStyle(new Color(255, 128, 128), Color.white,Isabelle.plugin.font) + array(6) = new SyntaxStyle(Color.yellow, Color.white, Isabelle.plugin.font) + array(7) = new SyntaxStyle( new Color(0, 192, 0), Color.white, Isabelle.plugin.font) + array(8) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font) + array(9) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font) + array(10) = new SyntaxStyle(Color.gray, Color.white, Isabelle.plugin.font) + array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font) + array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font) + array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font) + return array + } - private val kinds = List( - OuterKeyword.minor -> Token.KEYWORD4, - OuterKeyword.control -> Token.INVALID, - OuterKeyword.diag -> Token.LABEL, - OuterKeyword.heading -> Token.KEYWORD1, - OuterKeyword.theory1 -> Token.KEYWORD4, - OuterKeyword.theory2 -> Token.KEYWORD1, - OuterKeyword.proof1 -> Token.KEYWORD1, - OuterKeyword.proof2 -> Token.KEYWORD2, - OuterKeyword.improper -> Token.DIGIT - ) - def += (name: String, kind: String) = { - kinds.find(pair => pair._1.contains(kind)) match { - case None => - case Some((_, kind_byte)) => getMainRuleSet.getKeywords.add(name, kind_byte) + def choose_byte(kind: String): Byte = { + // TODO: as properties + kind match { + // logical entities + case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL + | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT + | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => 2 + // inner syntax + case Markup.TFREE | Markup.FREE => 3 + case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => 4 + case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL + | Markup.INNER_COMMENT => 5 + case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP + | Markup.ATTRIBUTE | Markup.METHOD => 6 + // embedded source text + case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ + | Markup.DOC_ANTIQ => 7 + // outer syntax + case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => 8 + case Markup.VERBATIM => 9 + case Markup.COMMENT => 10 + case Markup.CONTROL => 11 + case Markup.MALFORMED => 12 + case Markup.STRING | Markup.ALTSTRING => 13 + // other + case _ => 1 } } + + def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor + } + +class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker { + + override def markTokens(prev: TokenMarker.LineContext, + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = { + val previous = prev.asInstanceOf[IndexLineContext] + val line = if(prev == null) 0 else previous.line + 1 + val context = new IndexLineContext(line, previous) + val start = buffer.getLineStartOffset(line) + val stop = start + line_segment.count + + def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_) + def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_) + + val commands = document.commands.dropWhile(_.stop <= from(start)) + if(commands.hasNext) { + var next_x = start + for { + command <- commands.takeWhile(_.start < from(stop)) + markup <- command.root_node.flatten + if(to(markup.abs_stop) > start) + if(to(markup.abs_start) < stop) + byte = DynamicTokenMarker.choose_byte(markup.kind) + token_start = to(markup.abs_start) - start max 0 + token_length = to(markup.abs_stop) - to(markup.abs_start) - + (start - to(markup.abs_start) max 0) - + (to(markup.abs_stop) - stop max 0) + } { + if (start + token_start > next_x) + handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context) + handler.handleToken(line_segment, byte, token_start, token_length, context) + next_x = start + token_start + token_length + } + if (next_x < stop) + handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context) + } else { + handler.handleToken(line_segment, 1, 0, line_segment.count, context) + } + + handler.handleToken(line_segment,Token.END, line_segment.count, 0, context) + handler.setLineContext(context) + return context + } + +} + +class IndexLineContext(val line: Int, prev: IndexLineContext) + extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev) diff -r 73225f520f8c -r 163cda249619 src/Tools/jEdit/src/jedit/ProverSetup.scala --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Sun Feb 01 13:57:59 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Feb 02 23:05:25 2009 +0100 @@ -35,7 +35,7 @@ def activate(view: View) { prover = new Prover(Isabelle.system, Isabelle.default_logic) - + val buffer = view.getBuffer val dir = buffer.getDirectory @@ -73,13 +73,6 @@ state_panel.setDocument(state.result_document, UserAgent.baseURL) } }) - - // one independent token marker per prover - val token_marker = new DynamicTokenMarker - buffer.setTokenMarker(token_marker) - - // register for new declarations - prover.decl_info += (pair => token_marker += (pair._1, pair._2)) } diff -r 73225f520f8c -r 163cda249619 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Feb 01 13:57:59 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Feb 02 23:05:25 2009 +0100 @@ -35,35 +35,6 @@ case _ => Color.red } } - - def choose_color(markup: String): Color = { - // TODO: as properties - markup match { - // logical entities - case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL - | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT - | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255) - // inner syntax - case Markup.TFREE | Markup.FREE => Color.blue - case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green - case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL - | Markup.INNER_COMMENT => new Color(255, 128, 128) - case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP - | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow - // embedded source text - case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ - | Markup.DOC_ANTIQ => new Color(0, 192, 0) - // outer syntax - case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue - case Markup.VERBATIM => Color.green - case Markup.COMMENT => Color.gray - case Markup.CONTROL => Color.white - case Markup.MALFORMED => Color.red - case Markup.STRING | Markup.ALTSTRING => Color.orange - // other - case _ => Color.white - } - } } @@ -90,17 +61,13 @@ /* activation */ - Isabelle.plugin.font_changed += (_ => update_font()) + Isabelle.plugin.font_changed += (_ => update_styles) - private def update_font() = { + private def update_styles = { if (text_area != null) { if (Isabelle.plugin.font != null) { - val painter = text_area.getPainter - painter.setStyles(painter.getStyles.map(style => - new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font) - )) - painter.setFont(Isabelle.plugin.font) - repaint_all() + text_area.getPainter.setStyles(DynamicTokenMarker.styles) + repaint_all } } } @@ -119,7 +86,8 @@ phase_overview.textarea = text_area text_area.addLeftOfScrollBar(phase_overview) text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) - update_font() + buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document)) + update_styles } def deactivate() = { @@ -134,13 +102,13 @@ val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all()) prover.command_info += (_ => repaint_delay.delay_or_ignore()) - private def from_current(pos: Int) = + def from_current (pos: Int) = if (col != null && col.start <= pos) if (pos < col.start + col.added) col.start else pos - col.added + col.removed else pos - private def to_current(pos : Int) = + def to_current (pos : Int) = if (col != null && col.start <= pos) if (pos < col.start + col.removed) col.start else pos + col.added - col.removed @@ -206,8 +174,8 @@ val begin = to_current(node.start + e.start) val finish = to_current(node.stop + e.start) if (finish > start && begin < end) { - encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end, - TheoryView.choose_color(node.kind), true) + encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1, + DynamicTokenMarker.choose_color(node.kind), true) } } e = e.next diff -r 73225f520f8c -r 163cda249619 src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Feb 01 13:57:59 2009 +0100 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Feb 02 23:05:25 2009 +0100 @@ -94,12 +94,12 @@ val filled_gaps = for { child <- children markups = if (next_x < child.start) { - new MarkupNode(base, next_x, child.start, id, kind, desc) :: child.flatten + new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten } else child.flatten update = (next_x = child.stop) markup <- markups } yield markup - if (next_x <= stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, desc) + if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, "") else filled_gaps } } @@ -131,4 +131,5 @@ def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop + override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc }