# HG changeset patch
# User wenzelm
# Date 1345819417 -7200
# Node ID 9f84d872febaff0303b16ceae555bde9bff05981
# Parent  aaca64a7390c946ce183377f68c9af1653a3fca5
tuned signature;

diff -r aaca64a7390c -r 9f84d872feba src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Aug 24 13:05:14 2012 +0200
+++ b/src/Pure/General/position.scala	Fri Aug 24 16:43:37 2012 +0200
@@ -20,13 +20,32 @@
   val File = new Properties.String(Isabelle_Markup.FILE)
   val Id = new Properties.Long(Isabelle_Markup.ID)
 
+  object Line_File
+  {
+    def unapply(pos: T): Option[(Int, String)] =
+      (pos, pos) match {
+        case (Line(i), File(name)) => Some((i, name))
+        case (_, File(name)) => Some((1, name))
+        case _ => None
+      }
+  }
+
   object Range
   {
     def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
     def unapply(pos: T): Option[Text.Range] =
-      (Offset.unapply(pos), End_Offset.unapply(pos)) match {
-        case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
-        case (Some(start), None) => Some(Text.Range(start, start + 1))
+      (pos, pos) match {
+        case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
+        case (Offset(start), _) => Some(Text.Range(start, start + 1))
+        case _ => None
+      }
+  }
+
+  object Id_Offset
+  {
+    def unapply(pos: T): Option[(Long, Text.Offset)] =
+      (pos, pos) match {
+        case (Id(id), Offset(offset)) => Some((id, offset))
         case _ => None
       }
   }
@@ -52,8 +71,8 @@
       yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
 
 
-  def str_of(props: T): String =
-    (Line.unapply(props), File.unapply(props)) match {
+  def str_of(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) + ")"