diff -r 408a137e2793 -r f74672cf83c6 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sun Jan 07 20:32:36 2018 +0100
+++ b/src/Pure/General/scan.scala	Sun Jan 07 20:44:48 2018 +0100
@@ -203,17 +203,16 @@
 
     def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
     {
-      val depth =
-        ctxt match {
-          case Finished => 0
-          case Cartouche(d) => d
-          case _ => -1
-        }
-      if (depth >= 0)
-        cartouche_depth(depth) ^^
-          { case (x, 0) => (x, Finished)
-            case (x, d) => (x, Cartouche(d)) }
-      else failure("")
+      def cartouche_context(d: Int): Line_Context =
+        if (d == 0) Finished else Cartouche(d)
+
+      ctxt match {
+        case Finished =>
+          cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case Cartouche(depth) =>
+          cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case _ => failure("")
+      }
     }
 
     val recover_cartouche: Parser[String] =