# HG changeset patch
# User wenzelm
# Date 1397201798 -7200
# Node ID 3da244bc02bde8375c39bfe991669f48bb9994a3
# Parent  ec4cd116844bc29126b565d19db32906a47efb72
tuned message, to accommodate extra brackets produced by Scala parsers;

diff -r ec4cd116844b -r 3da244bc02bd src/Pure/General/position.ML
--- 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
diff -r ec4cd116844b -r 3da244bc02bd 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 _ => ""
+    }
 }
diff -r ec4cd116844b -r 3da244bc02bd src/Pure/Isar/token.scala
--- 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]