--- 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
--- 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)
--- 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) {
--- 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)
+
}
--- 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 _ =>