--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 15:15:15 2009 +0200
@@ -115,7 +115,7 @@
var next_x = start
while (command != null && command.start(document) < from(stop)) {
for {
- markup <- command.highlight_node.flatten
+ markup <- command.highlight_node(document).flatten
if (to(markup.abs_stop(document)) > start)
if (to(markup.abs_start(document)) < stop)
byte = DynamicTokenMarker.choose_byte(markup.info.toString)