src/Pure/General/scan.scala

--- a/src/Pure/General/scan.scala	Sat Jan 09 22:41:08 2021 +0100
+++ b/src/Pure/General/scan.scala	Sun Jan 10 13:04:29 2021 +0100
@@ -107,7 +107,7 @@
 
     def quoted_content(quote: Symbol.Symbol, source: String): String =
     {
-      require(parseAll(quoted(quote), source).successful)
+      require(parseAll(quoted(quote), source).successful, "no quoted text")
       val body = source.substring(1, source.length - 1)
       if (body.exists(_ == '\\')) {
         val content =
@@ -149,7 +149,7 @@
 
     def verbatim_content(source: String): String =
     {
-      require(parseAll(verbatim, source).successful)
+      require(parseAll(verbatim, source).successful, "no verbatim text")
       source.substring(2, source.length - 2)
     }
 
@@ -176,7 +176,7 @@
 
     def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
     {
-      require(depth >= 0)
+      require(depth >= 0, "bad cartouche depth")
 
       def apply(in: Input) =
       {
@@ -235,7 +235,7 @@
 
     private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
     {
-      require(depth >= 0)
+      require(depth >= 0, "bad comment depth")
 
       val comment_text: Parser[List[String]] =
         rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
@@ -286,7 +286,7 @@
 
     def comment_content(source: String): String =
     {
-      require(parseAll(comment, source).successful)
+      require(parseAll(comment, source).successful, "no comment")
       source.substring(2, source.length - 2)
     }