author | wenzelm |
Thu, 06 Apr 2017 13:30:46 +0200 | |
changeset 65402 | 37d3657e8513 |
parent 65401 | 590c1a53c78d |
child 65403 | 4a042bf9488e |
--- 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) ""