diff -r d8dc8fdc46fc -r 6e4093927dbb src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Isar/token.scala	Tue Sep 28 16:01:13 2021 +0200
@@ -34,6 +34,7 @@
     val ALT_STRING = Value("back-quoted string")
     val VERBATIM = Value("verbatim text")
     val CARTOUCHE = Value("text cartouche")
+    val CONTROL = Value("control cartouche")
     val INFORMAL_COMMENT = Value("informal comment")
     val FORMAL_COMMENT = Value("formal comment")
     /*special content*/
@@ -53,11 +54,12 @@
       val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
       val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
       val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
-      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
       val cmt = comment ^^ (x => Token(Token.Kind.INFORMAL_COMMENT, x))
       val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x))
+      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
+      val ctrl = control_cartouche ^^ (x => Token(Token.Kind.CONTROL, x))
 
-      string | (alt_string | (verb | (cart | (cmt | formal_cmt))))
+      string | (alt_string | (verb | (cmt | (formal_cmt | (cart | ctrl)))))
     }
 
     private def other_token(keywords: Keyword.Keywords): Parser[Token] =