src/Pure/Isar/token.scala
changeset 59695 a03e0561bdbf
parent 59671 9715eb8e9408
child 59696 f505fee04400
     1.1 --- a/src/Pure/Isar/token.scala	Sat Mar 14 18:18:40 2015 +0100
     1.2 +++ b/src/Pure/Isar/token.scala	Sat Mar 14 19:51:36 2015 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4        else new Pos(line1, offset1, file, id)
     1.5      }
     1.6  
     1.7 -    def position(end_offset: Symbol.Offset): Position.T =
     1.8 +    private def position(end_offset: Symbol.Offset): Position.T =
     1.9        (if (line > 0) Position.Line(line) else Nil) :::
    1.10        (if (offset > 0) Position.Offset(offset) else Nil) :::
    1.11        (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
    1.12 @@ -204,7 +204,7 @@
    1.13      def atEnd = tokens.isEmpty
    1.14    }
    1.15  
    1.16 -  def reader(tokens: List[Token], file: String = "", id: Document_ID.Generic = Document_ID.none)
    1.17 +  def reader(tokens: List[Token], file: String, id: Document_ID.Generic = Document_ID.none)
    1.18      : Reader = new Token_Reader(tokens, new Pos(1, 1, file, id))
    1.19  }
    1.20