# HG changeset patch
# User wenzelm
# Date 1672400089 -3600
# Node ID 919b0f21e8cca553404075331d2ce170ef67c93f
# Parent  8a17349143df036db561f28b5333ea46ce6f5c17
tuned;

diff -r 8a17349143df -r 919b0f21e8cc src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Thu Dec 29 22:14:25 2022 +0000
+++ b/src/Pure/PIDE/line.scala	Fri Dec 30 12:34:49 2022 +0100
@@ -48,7 +48,7 @@
         val lines = logical_lines(text)
         val l = line + lines.length - 1
         val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length
-        Position(l, c)
+        Position(line = l, column = c)
       }
   }
 
@@ -61,8 +61,9 @@
   }
 
   sealed case class Range(start: Position, stop: Position) {
-    if (start.compare(stop) > 0)
+    if (start.compare(stop) > 0) {
       error("Bad line range: " + start.print + ".." + stop.print)
+    }
 
     def print: String =
       if (start == stop) start.print
@@ -73,7 +74,7 @@
   /* positions within document node */
 
   object Node_Position {
-    def offside(name: String): Node_Position = Node_Position(name, Position.offside)
+    def offside(name: String): Node_Position = Node_Position(name, pos = Position.offside)
   }
 
   sealed case class Node_Position(name: String, pos: Position = Position.zero) {
@@ -134,11 +135,14 @@
     def position(text_offset: Text.Offset): Position = {
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = {
         lines_rest match {
-          case Nil => require(i == 0, "bad Line.position.move"); Position(lines_count)
+          case Nil =>
+            require(i == 0, "bad Line.position.move")
+            Position(line = lines_count)
           case line :: ls =>
             val n = line.text.length
-            if (ls.isEmpty || i <= n)
-              Position(lines_count).advance(line.text.substring(n - i))
+            if (ls.isEmpty || i <= n) {
+              Position(line = lines_count).advance(line.text.substring(n - i))
+            }
             else move(i - (n + 1), lines_count + 1, ls)
         }
       }