src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
changeset 34717 3f32e08bbb6c
parent 34712 4f0ee5ab0380
child 34727 3ec545c964d5
equal deleted inserted replaced
34716:b8f2b44529fd 34717:3f32e08bbb6c
   124     var next_x = start
   124     var next_x = start
   125     var cmd = document.command_at(from(start))
   125     var cmd = document.command_at(from(start))
   126     while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
   126     while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
   127       val command = cmd.get
   127       val command = cmd.get
   128       for {
   128       for {
   129         markup <- command.highlight_node(document).flatten
   129         markup <- command.highlight(document).flatten
   130         command_start = command.start(document)
   130         command_start = command.start(document)
   131         abs_start = to(command_start + markup.start)
   131         abs_start = to(command_start + markup.start)
   132         abs_stop = to(command_start + markup.stop)
   132         abs_stop = to(command_start + markup.stop)
   133         if (abs_stop > start)
   133         if (abs_stop > start)
   134         if (abs_start < stop)
   134         if (abs_start < stop)