# 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)))
     }