tuned signature;
authorwenzelm
Tue Aug 12 00:23:30 2014 +0200 (2014-08-12)
changeset 579077fc36b4c7cce
parent 57906 020df63dd0a9
child 57908 1937603dbdf2
tuned signature;
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:23:30 2014 +0200
     1.3 @@ -124,18 +124,16 @@
     1.4  
     1.5    /* token language */
     1.6  
     1.7 -  def scan(input: Reader[Char]): List[Token] =
     1.8 +  def scan(input: CharSequence): List[Token] =
     1.9    {
    1.10 +    var in: Reader[Char] = new CharSequenceReader(input)
    1.11      Token.Parsers.parseAll(
    1.12 -        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
    1.13 +        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
    1.14        case Token.Parsers.Success(tokens, _) => tokens
    1.15 -      case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    1.16 +      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
    1.17      }
    1.18    }
    1.19  
    1.20 -  def scan(input: CharSequence): List[Token] =
    1.21 -    scan(new CharSequenceReader(input))
    1.22 -
    1.23    def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
    1.24    {
    1.25      var in: Reader[Char] = new CharSequenceReader(input)