src/Pure/General/position.scala
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) ""