--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Sep 06 22:27:32 2009 +0200
@@ -126,7 +126,7 @@
while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
val command = cmd.get
for {
- markup <- command.highlight_node(document).flatten
+ markup <- command.highlight(document).flatten
command_start = command.start(document)
abs_start = to(command_start + markup.start)
abs_stop = to(command_start + markup.stop)