tuned;
authorwenzelm
Tue Dec 20 09:52:01 2016 +0100 (2016-12-20)
changeset 6461208e4b1aeac50
parent 64611 d72d63d05bdb
child 64613 d1ca9ce0d9e4
tuned;
src/Pure/General/symbol.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/General/symbol.scala	Tue Dec 20 08:57:03 2016 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Dec 20 09:52:01 2016 +0100
     1.3 @@ -128,16 +128,6 @@
     1.4  
     1.5    def explode(text: CharSequence): List[Symbol] = iterator(text).toList
     1.6  
     1.7 -  def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
     1.8 -  {
     1.9 -    var (line, column) = pos
    1.10 -    for (sym <- iterator(text)) {
    1.11 -      if (is_newline(sym)) { line += 1; column = 1 }
    1.12 -      else column += 1
    1.13 -    }
    1.14 -    (line, column)
    1.15 -  }
    1.16 -
    1.17  
    1.18    /* decoding offsets */
    1.19  
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 08:57:03 2016 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 09:52:01 2016 +0100
     2.3 @@ -269,14 +269,13 @@
     2.4        case Some(name) =>
     2.5          JEdit_Lib.jedit_buffer(name) match {
     2.6            case Some(buffer) if offset > 0 =>
     2.7 -            val (line, column) =
     2.8 +            val pos =
     2.9                JEdit_Lib.buffer_lock(buffer) {
    2.10 -                ((1, 1) /:
    2.11 +                (Line.Position.zero /:
    2.12                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    2.13 -                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    2.14 -                      Symbol.advance_line_column)
    2.15 +                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance_symbols(_))
    2.16                }
    2.17 -            Some(hyperlink_file(focus, name, line, column))
    2.18 +            Some(hyperlink_file(focus, name, pos.line1, pos.column1))
    2.19            case _ => Some(hyperlink_file(focus, name, line))
    2.20          }
    2.21        case None => None
    2.22 @@ -297,8 +296,8 @@
    2.23              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    2.24                (if (offset == 0) Iterator.empty
    2.25                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
    2.26 -          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    2.27 -          Some(hyperlink_file(focus, file_name, line, column))
    2.28 +          val pos = (Line.Position.zero /: sources_iterator)(_.advance_symbols(_))
    2.29 +          Some(hyperlink_file(focus, file_name, pos.line1, pos.column1))
    2.30        }
    2.31      }
    2.32    }