# 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) } }