# HG changeset patch # User wenzelm # Date 1308313873 -7200 # Node ID a26e514c92b29c1c9e9a77c2051f1aa09f3446ba # Parent 6ed49c52d4635e2e41a92e0dc616dd57a58d8ae7 unconditional recovery from bad context (e.g. Quoted with malformed quoted_body); diff -r 6ed49c52d463 -r a26e514c92b2 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri Jun 17 13:55:53 2011 +0200 +++ b/src/Pure/General/scan.scala Fri Jun 17 14:31:13 2011 +0200 @@ -388,12 +388,7 @@ quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } - - val other: Parser[(Token, Context)] = - ctxt match { - case Finished => other_token(symbols, is_command) ^^ { case x => (x, Finished) } - case _ => failure("") - } + val other = other_token(symbols, is_command) ^^ { case x => (x, Finished) } string | (alt_string | (verb | (cmt | other))) }