proper default (amending 601866c61ded);
authorwenzelm
Thu, 06 Apr 2017 13:30:46 +0200
changeset 65402 37d3657e8513
parent 65401 590c1a53c78d
child 65403 4a042bf9488e
proper default (amending 601866c61ded);
src/Pure/General/position.scala
--- 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) ""