proper counting of chars;
authorwenzelm
Tue Dec 20 10:01:53 2016 +0100 (2016-12-20)
changeset 64613d1ca9ce0d9e4
parent 64612 08e4b1aeac50
child 64614 88211daacf93
proper counting of chars;
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 09:52:01 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 10:01:53 2016 +0100
     1.3 @@ -273,7 +273,7 @@
     1.4                JEdit_Lib.buffer_lock(buffer) {
     1.5                  (Line.Position.zero /:
     1.6                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
     1.7 -                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance_symbols(_))
     1.8 +                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
     1.9                }
    1.10              Some(hyperlink_file(focus, name, pos.line1, pos.column1))
    1.11            case _ => Some(hyperlink_file(focus, name, line))
    1.12 @@ -296,7 +296,7 @@
    1.13              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.14                (if (offset == 0) Iterator.empty
    1.15                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
    1.16 -          val pos = (Line.Position.zero /: sources_iterator)(_.advance_symbols(_))
    1.17 +          val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
    1.18            Some(hyperlink_file(focus, file_name, pos.line1, pos.column1))
    1.19        }
    1.20      }