1.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Dec 07 18:20:33 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Dec 07 20:39:09 2012 +0100
     1.3 @@ -112,32 +112,34 @@
     1.4    /* tokenize */
     1.5  
     1.6    def scan(input: Reader[Char]): List[Token] =
     1.7 -  {
     1.8 -    import lexicon._
     1.9 +    Exn.recover  // FIXME !?
    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 +      parseAll(rep(token(is_command)), input) match {
    1.17 +        case Success(tokens, _) => tokens
    1.18 +        case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    1.19 +      }
    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 -  {
    1.28 -    import lexicon._
    1.29 +    Exn.recover  // FIXME !?
    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 +      var in: Reader[Char] = new CharSequenceReader(input)
    1.42 +      val toks = new mutable.ListBuffer[Token]
    1.43 +      var ctxt = context
    1.44 +      while (!in.atEnd) {
    1.45 +        parse(token_context(is_command, ctxt), in) match {
    1.46 +          case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    1.47 +          case NoSuccess(_, rest) =>
    1.48 +            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.49 +        }
    1.50        }
    1.51 +      (toks.toList, ctxt)
    1.52      }
    1.53 -    (toks.toList, ctxt)
    1.54 -  }
    1.55  }