src/Tools/jEdit/src/jedit/document_model.scala
changeset 38427 7066fbd315ae
parent 38426 2858ec7b6dd8
child 38479 e628da370072
     1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 22:48:56 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 23:07:22 2010 +0200
     1.3 @@ -280,8 +280,7 @@
     1.4          (command, command_start) <-
     1.5            snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
     1.6          markup <- snapshot.state(command).highlight.flatten
     1.7 -        val abs_start = snapshot.convert(command_start + markup.range.start)
     1.8 -        val abs_stop = snapshot.convert(command_start + markup.range.stop)
     1.9 +        val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
    1.10          if (abs_stop > start)
    1.11          if (abs_start < stop)
    1.12          val token_start = (abs_start - start) max 0