# HG changeset patch
# User immler@in.tum.de
# Date 1240846429 -7200
# Node ID 09a5984250a21e51035a73b73006df36c7fcbe58
# Parent  7c001369956abb9e2c02c09044442fa3cb77fb0d
seperate node for syntax-highlighting

diff -r 7c001369956a -r 09a5984250a2 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Mon Apr 27 14:03:05 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Mon Apr 27 17:33:49 2009 +0200
@@ -25,5 +25,6 @@
 view.showToolbar=false
 buffer.sidekick.keystroke-parse=true
 sidekick.buffer-save-parse=true
+mode.isabelle.sidekick.showStatusWindow.label=true
 sidekick-tree.dock-position=right
 isabelle-state.dock-position=bottom
diff -r 7c001369956a -r 09a5984250a2 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 27 14:03:05 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 27 17:33:49 2009 +0200
@@ -82,7 +82,7 @@
     var next_x = start
     for {
       command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
-      markup <- command.root_node.flatten
+      markup <- command.highlight_node.flatten
       if(to(markup.abs_stop(document)) > start)
       if(to(markup.abs_start(document)) < stop)
       byte = DynamicTokenMarker.choose_byte(markup.desc)
diff -r 7c001369956a -r 09a5984250a2 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 27 14:03:05 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 27 17:33:49 2009 +0200
@@ -199,7 +199,7 @@
       encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
 
       // paint details of command
-      for (node <- e.root_node.dfs) {
+      for (node <- e.highlight_node.flatten) {
         val begin = to_current(node.abs_start(document))
         val finish = to_current(node.abs_stop(document))
         if (finish > start && begin < end) {
diff -r 7c001369956a -r 09a5984250a2 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Apr 27 14:03:05 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Apr 27 17:33:49 2009 +0200
@@ -80,7 +80,7 @@
   /* markup */
 
   val root_node =
-    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, Markup.COMMAND_SPAN, content)
+    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, content, Markup.COMMAND_SPAN)
 
   def add_markup(desc: String, begin: Int, end: Int) = {
     val markup_content = if (end <= content.length) content.substring(begin, end)
@@ -90,4 +90,12 @@
       }
     root_node insert new MarkupNode(this, begin, end, id, markup_content, desc)
   }
+
+  // syntax highlighting
+  val highlight_node =
+   new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, content, Markup.COMMAND_SPAN)
+
+  def add_highlight(kind: String, begin: Int, end: Int) =
+    highlight_node insert new MarkupNode(this, begin, end, id, "", kind)
+
 }
diff -r 7c001369956a -r 09a5984250a2 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 27 14:03:05 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 27 17:33:49 2009 +0200
@@ -195,7 +195,7 @@
                     val markup_id = get_attr(attr, Markup.ID).get
                     command.add_markup(body.toString, begin, end)
                     command_change(command)
-                  // other markup
+                  // syntax highlighting
                   case XML.Elem(kind, attr, body) =>
                     val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
                     val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
@@ -208,6 +208,7 @@
                       else command
                     if (cmd != null) {
                       cmd.add_markup(kind, begin, end)
+                      cmd.add_highlight(kind, begin, end)
                       command_change(cmd)
                     }
                   case _ =>