implemented markTokens;
moved choose_color to DynamicTokenMarker and extended to choose_style

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

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

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

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