src/Tools/jEdit/src/jedit_editor.scala
changeset 64612 08e4b1aeac50
parent 64524 e6a3c55b929b
child 64613 d1ca9ce0d9e4
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 08:57:03 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 09:52:01 2016 +0100
     1.3 @@ -269,14 +269,13 @@
     1.4        case Some(name) =>
     1.5          JEdit_Lib.jedit_buffer(name) match {
     1.6            case Some(buffer) if offset > 0 =>
     1.7 -            val (line, column) =
     1.8 +            val pos =
     1.9                JEdit_Lib.buffer_lock(buffer) {
    1.10 -                ((1, 1) /:
    1.11 +                (Line.Position.zero /:
    1.12                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    1.13 -                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    1.14 -                      Symbol.advance_line_column)
    1.15 +                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance_symbols(_))
    1.16                }
    1.17 -            Some(hyperlink_file(focus, name, line, column))
    1.18 +            Some(hyperlink_file(focus, name, pos.line1, pos.column1))
    1.19            case _ => Some(hyperlink_file(focus, name, line))
    1.20          }
    1.21        case None => None
    1.22 @@ -297,8 +296,8 @@
    1.23              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.24                (if (offset == 0) Iterator.empty
    1.25                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
    1.26 -          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    1.27 -          Some(hyperlink_file(focus, file_name, line, column))
    1.28 +          val pos = (Line.Position.zero /: sources_iterator)(_.advance_symbols(_))
    1.29 +          Some(hyperlink_file(focus, file_name, pos.line1, pos.column1))
    1.30        }
    1.31      }
    1.32    }