# HG changeset patch
# User wenzelm
# Date 1482940958 -3600
# Node ID 642b6105e6f4012adb88862eb2c96a44040bba75
# Parent  7f87c1aa0ffa185bc905465f03bf6a5261b367f5
clarified signature: explicit Length to avoid implicit mistakes;

diff -r 7f87c1aa0ffa -r 642b6105e6f4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Dec 28 16:50:14 2016 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Dec 28 17:02:38 2016 +0100
@@ -808,7 +808,7 @@
               node.commands.iterator.takeWhile(_ != command).map(_.source) ++
                 (if (offset == 0) Iterator.empty
                  else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Length))
             Line.Node_Position(name, pos)
           }
 
diff -r 7f87c1aa0ffa -r 642b6105e6f4 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 28 16:50:14 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 17:02:38 2016 +0100
@@ -31,12 +31,12 @@
         case i => i
       }
 
-    def advance(text: String, length: Length = Length): Position =
+    def advance(text: String, text_length: Length): Position =
       if (text.isEmpty) this
       else {
         val lines = Library.split_lines(text)
         val l = line + lines.length - 1
-        val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
+        val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
         Position(l, c)
       }
   }
@@ -107,7 +107,7 @@
       }
     override def hashCode(): Int = lines.hashCode
 
-    def position(offset: Text.Offset, length: Length = Length): Position =
+    def position(text_offset: Text.Offset, text_length: Length): Position =
     {
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
       {
@@ -116,27 +116,27 @@
           case line :: ls =>
             val n = line.text.length
             if (ls.isEmpty || i <= n)
-              Position(lines_count).advance(line.text.substring(n - i), length)
+              Position(lines_count).advance(line.text.substring(n - i), text_length)
             else move(i - (n + 1), lines_count + 1, ls)
         }
       }
-      move(offset, 0, lines)
+      move(text_offset, 0, lines)
     }
 
-    def range(text_range: Text.Range, length: Length = Length): Range =
+    def range(text_range: Text.Range, text_length: Length): Range =
       Range(
-        position(text_range.start, length),
-        position(text_range.stop, length))
+        position(text_range.start, text_length),
+        position(text_range.stop, text_length))
 
-    def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
+    def offset(pos: Position, text_length: Length): Option[Text.Offset] =
     {
       val l = pos.line
       val c = pos.column
       if (0 <= l && l < lines.length) {
         val line_offset =
           if (l == 0) 0
-          else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
-        length.offset(lines(l).text, c).map(line_offset + _)
+          else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
+        text_length.offset(lines(l).text, c).map(line_offset + _)
       }
       else None
     }
diff -r 7f87c1aa0ffa -r 642b6105e6f4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 16:50:14 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 17:02:38 2016 +0100
@@ -270,7 +270,7 @@
             JEdit_Lib.buffer_lock(buffer) {
               (Line.Position.zero /:
                 (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
+                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_, Length))
             }
           hyperlink_file(focus, Line.Node_Position(name, pos))
         case _ =>