src/Pure/General/position.scala

--- a/src/Pure/General/position.scala	Thu Apr 10 18:29:32 2014 +0200
+++ b/src/Pure/General/position.scala	Fri Apr 11 09:36:38 2014 +0200
@@ -99,7 +99,7 @@
   def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
 
 
-  /* here: inlined formal markup */
+  /* here: user output */
 
   def here(pos: T): String =
     (Line.unapply(pos), File.unapply(pos)) match {
@@ -108,4 +108,12 @@
       case (None, Some(name)) => " (file " + quote(name) + ")"
       case _ => ""
     }
+
+  def here_undelimited(pos: T): String =
+    (Line.unapply(pos), File.unapply(pos)) match {
+      case (Some(i), None) => "line " + i.toString
+      case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
+      case (None, Some(name)) => "file " + quote(name)
+      case _ => ""
+    }
 }