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