# HG changeset patch
# User wenzelm
# Date 1483214443 -3600
# Node ID 601866c61ded3e82788bc73501023570c34913ff
# Parent  13e37567a0d6c339f2fcc61aa9955b1d680c3510
more precise markup;
tuned signature;

diff -r 13e37567a0d6 -r 601866c61ded src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sat Dec 31 20:26:34 2016 +0100
+++ b/src/Pure/General/position.scala	Sat Dec 31 21:00:43 2016 +0100
@@ -132,21 +132,20 @@
 
   /* here: user output */
 
-  def here(pos: T): String =
-    Markup(Markup.POSITION, pos).markup(
-      (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 _ => ""
-      })
-
-  def here_undelimited(pos: T): String =
-    Markup(Markup.POSITION, pos).markup(
-      (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 _ => ""
-      })
+  def here(props: T, delimited: Boolean = false): String =
+  {
+    val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1))
+    if (pos.isEmpty) ""
+    else {
+      val s0 =
+        (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 _ => ""
+        }
+      val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else " " + s0
+      Markup(Markup.POSITION, pos).markup(s)
+    }
+  }
 }
diff -r 13e37567a0d6 -r 601866c61ded src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Dec 31 20:26:34 2016 +0100
+++ b/src/Pure/Isar/token.scala	Sat Dec 31 21:00:43 2016 +0100
@@ -207,7 +207,7 @@
     def position(): Position.T = position(0)
     def position(token: Token): Position.T = position(advance(token).offset)
 
-    override def toString: String = Position.here_undelimited(position())
+    override def toString: String = Position.here(position(), delimited = false)
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]