tuned message, to accommodate extra brackets produced by Scala parsers;

--- a/src/Pure/General/position.ML	Thu Apr 10 18:29:32 2014 +0200
+++ b/src/Pure/General/position.ML	Fri Apr 11 09:36:38 2014 +0200
@@ -191,7 +191,7 @@
   Unsynchronized.change r (append (map (rpair "") reports));
 
 
-(* here: inlined formal markup *)
+(* here: user output *)
 
 fun here pos =
   let

--- 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 _ => ""
+    }
 }

--- a/src/Pure/Isar/token.scala	Thu Apr 10 18:29:32 2014 +0200
+++ b/src/Pure/Isar/token.scala	Fri Apr 11 09:36:38 2014 +0200
@@ -140,7 +140,7 @@
     }
 
     def position: Position.T = Position.Line_File(line, file)
-    override def toString: String = Position.here(position)
+    override def toString: String = Position.here_undelimited(position)
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]