--- 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)