src/Pure/General/position.scala
changeset 68287 2ae74a278c10
parent 67882 7eb4c966e156
child 72692 22aeec526ffd
--- a/src/Pure/General/position.scala	Sat May 26 10:11:11 2018 +0100
+++ b/src/Pure/General/position.scala	Sat May 26 13:34:44 2018 +0200
@@ -144,7 +144,7 @@
           case (None, Some(name)) => "file " + quote(name)
           case _ => ""
         }
-      val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else " " + s0
+      val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
       Markup(Markup.POSITION, pos).markup(s)
     }
   }