# HG changeset patch
# User wenzelm
# Date 1672400468 -3600
# Node ID 65e8a9272837157018d13a25fb092bab2ae5e0f2
# Parent  919b0f21e8cca553404075331d2ce170ef67c93f
clarified output;

diff -r 919b0f21e8cc -r 65e8a9272837 src/Pure/PIDE/line.scala
--- 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 {