src/Tools/jEdit/src/jedit/document_view.scala
changeset 38426 2858ec7b6dd8
parent 38360 53224a4d2f0e
child 38429 9951852fae91
     1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 15 21:42:13 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 15 22:48:56 2010 +0200
     1.3 @@ -152,12 +152,12 @@
     1.4  
     1.5        val snapshot = model.snapshot()
     1.6  
     1.7 -      val command_range: Iterable[(Command, Int)] =
     1.8 +      val command_range: Iterable[(Command, Text.Offset)] =
     1.9        {
    1.10          val range = snapshot.node.command_range(snapshot.revert(start(0)))
    1.11          if (range.hasNext) {
    1.12            val (cmd0, start0) = range.next
    1.13 -          new Iterable[(Command, Int)] {
    1.14 +          new Iterable[(Command, Text.Offset)] {
    1.15              def iterator =
    1.16                Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
    1.17            }