author | wenzelm |
Fri, 30 Dec 2022 12:41:08 +0100 | |
changeset 76825 | 65e8a9272837 |
parent 76824 | 919b0f21e8cc |
child 76826 | eb3b946bdeff |
--- a/src/Pure/PIDE/line.scala Fri Dec 30 12:34:49 2022 +0100 +++ b/src/Pure/PIDE/line.scala Fri Dec 30 12:41:08 2022 +0100 @@ -34,7 +34,9 @@ sealed case class Position(line: Int = 0, column: Int = 0) { def line1: Int = line + 1 def column1: Int = column + 1 - def print: String = line1.toString + ":" + column1.toString + def print: String = + if (column == 0) line1.toString + else line1.toString + ":" + column1.toString def compare(that: Position): Int = line compare that.line match {