tuned output;
authorwenzelm
Sat, 26 May 2018 13:34:44 +0200
changeset 68287 2ae74a278c10
parent 68286 b9160ca067ae
child 68288 d20770229f99
tuned output;
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)
     }
   }