# HG changeset patch
# User wenzelm
# Date 1426360083 -3600
# Node ID f505fee044002211c1e800d66be7e7623bafc1ae
# Parent  a03e0561bdbf3d6cb7a2fa7328cc924defa82cd1
tuned signature;

diff -r a03e0561bdbf -r f505fee04400 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Mar 14 19:51:36 2015 +0100
+++ b/src/Pure/Isar/token.scala	Sat Mar 14 20:08:03 2015 +0100
@@ -157,14 +157,14 @@
 
   object Pos
   {
-    val none: Pos = new Pos()
+    val none: Pos = new Pos(0, 0, "")
+    def file(file: String): Pos = new Pos(0, 0, file)
   }
 
   final class Pos private[Token](
-      val line: Int = 0,
-      val offset: Symbol.Offset = 0,
-      val file: String = "",
-      val id: Document_ID.Generic = Document_ID.none)
+      val line: Int,
+      val offset: Symbol.Offset,
+      val file: String)
     extends scala.util.parsing.input.Position
   {
     def column = 0
@@ -179,15 +179,14 @@
         if (offset1 > 0) offset1 += 1
       }
       if (line1 == line && offset1 == offset) this
-      else new Pos(line1, offset1, file, id)
+      else new Pos(line1, offset1, file)
     }
 
     private def position(end_offset: Symbol.Offset): Position.T =
       (if (line > 0) Position.Line(line) else Nil) :::
       (if (offset > 0) Position.Offset(offset) else Nil) :::
       (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
-      (if (file != "") Position.File(file) else Nil) :::
-      (if (id != Document_ID.none) Position.Id(id) else Nil)
+      (if (file != "") Position.File(file) else Nil)
 
     def position(): Position.T = position(0)
     def position(token: Token): Position.T = position(advance(token).offset)
@@ -204,8 +203,8 @@
     def atEnd = tokens.isEmpty
   }
 
-  def reader(tokens: List[Token], file: String, id: Document_ID.Generic = Document_ID.none)
-    : Reader = new Token_Reader(tokens, new Pos(1, 1, file, id))
+  def reader(tokens: List[Token], file: String): Reader =
+    new Token_Reader(tokens, Pos.file(file))
 }