# HG changeset patch
# User wenzelm
# Date 1344628400 -7200
# Node ID de68fc11c2456a5d4e4118c6a7315856b2890673
# Parent  9ff86bf6ad19582407f64eaccdd3908e18f0cb19
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;

diff -r 9ff86bf6ad19 -r de68fc11c245 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Aug 10 21:22:40 2012 +0200
+++ b/src/Pure/General/scan.scala	Fri Aug 10 21:53:20 2012 +0200
@@ -235,8 +235,8 @@
       }
     }.named("quoted_context")
 
-    def quoted_prefix(quote: Symbol.Symbol): Parser[String] =
-      quoted_context(quote, Finished) ^^ (_._1)
+    def recover_quoted(quote: Symbol.Symbol): Parser[String] =
+      quote ~ quoted_body(quote) ^^ { case x ~ y => x + y }
 
 
     /* verbatim text */
@@ -270,8 +270,8 @@
       }
     }.named("verbatim_context")
 
-    val verbatim_prefix: Parser[String] =
-      verbatim_context(Finished) ^^ (_._1)
+    val recover_verbatim: Parser[String] =
+      "{*" ~ verbatim_body ^^ { case x ~ y => x + y }
 
 
     /* nested comments */
@@ -329,8 +329,8 @@
       else failure("")
     }
 
-    val comment_prefix: Parser[String] =
-      comment_context(Finished) ^^ (_._1)
+    val recover_comment: Parser[String] =
+      comment_depth(0) ^^ (_._1)
 
 
     /* outer syntax tokens */
@@ -374,7 +374,7 @@
       val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
 
       val recover_delimited =
-        (quoted_prefix("\"") | (quoted_prefix("`") | (verbatim_prefix | comment_prefix))) ^^
+        (recover_quoted("\"") | (recover_quoted("`") | (recover_verbatim | recover_comment))) ^^
           (x => Token(Token.Kind.ERROR, x))
 
       val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))