# HG changeset patch
# User wenzelm
# Date 1527334484 -7200
# Node ID 2ae74a278c10ce629e2baa5c09855bdc7d2e5022
# Parent  b9160ca067ae3a4e2254c0cad8257867da6b374d
tuned output;

diff -r b9160ca067ae -r 2ae74a278c10 src/Pure/General/position.scala
--- 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)
     }
   }