changeset 65402 | 37d3657e8513 |
parent 64728 | 601866c61ded |
child 67882 | 7eb4c966e156 |
--- a/src/Pure/General/position.scala Thu Apr 06 11:23:26 2017 +0200 +++ b/src/Pure/General/position.scala Thu Apr 06 13:30:46 2017 +0200 @@ -132,7 +132,7 @@ /* here: user output */ - def here(props: T, delimited: Boolean = false): String = + def here(props: T, delimited: Boolean = true): String = { val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1)) if (pos.isEmpty) ""