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