src/Pure/Isar/outer_syntax.scala
changeset 52066 83b7b88770c9
parent 50428 7a78a74139f5
child 52439 4cf3f6153eb8
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat May 18 12:41:31 2013 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat May 18 13:00:05 2013 +0200
     1.3 @@ -112,34 +112,32 @@
     1.4    /* tokenize */
     1.5  
     1.6    def scan(input: Reader[Char]): List[Token] =
     1.7 -    Exn.recover  // FIXME !?
     1.8 -    {
     1.9 -      import lexicon._
    1.10 +  {
    1.11 +    import lexicon._
    1.12  
    1.13 -      parseAll(rep(token(is_command)), input) match {
    1.14 -        case Success(tokens, _) => tokens
    1.15 -        case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    1.16 -      }
    1.17 +    parseAll(rep(token(is_command)), input) match {
    1.18 +      case Success(tokens, _) => tokens
    1.19 +      case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    1.20      }
    1.21 +  }
    1.22  
    1.23    def scan(input: CharSequence): List[Token] =
    1.24      scan(new CharSequenceReader(input))
    1.25  
    1.26    def scan_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) =
    1.27 -    Exn.recover  // FIXME !?
    1.28 -    {
    1.29 -      import lexicon._
    1.30 +  {
    1.31 +    import lexicon._
    1.32  
    1.33 -      var in: Reader[Char] = new CharSequenceReader(input)
    1.34 -      val toks = new mutable.ListBuffer[Token]
    1.35 -      var ctxt = context
    1.36 -      while (!in.atEnd) {
    1.37 -        parse(token_context(is_command, ctxt), in) match {
    1.38 -          case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    1.39 -          case NoSuccess(_, rest) =>
    1.40 -            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.41 -        }
    1.42 +    var in: Reader[Char] = new CharSequenceReader(input)
    1.43 +    val toks = new mutable.ListBuffer[Token]
    1.44 +    var ctxt = context
    1.45 +    while (!in.atEnd) {
    1.46 +      parse(token_context(is_command, ctxt), in) match {
    1.47 +        case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    1.48 +        case NoSuccess(_, rest) =>
    1.49 +          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.50        }
    1.51 -      (toks.toList, ctxt)
    1.52      }
    1.53 +    (toks.toList, ctxt)
    1.54 +  }
    1.55  }