src/Pure/General/antiquote.scala
changeset 77011 3e48f8c6afc9
parent 75420 73a2f3fe0e8c
--- a/src/Pure/General/antiquote.scala	Wed Jan 18 16:49:01 2023 +0100
+++ b/src/Pure/General/antiquote.scala	Thu Jan 19 11:23:44 2023 +0100
@@ -38,6 +38,11 @@
 
     val antiquote: Parser[Antiquote] =
       txt ^^ (x => Text(x)) | (control ^^ (x => Control(x)) | antiq ^^ (x => Antiq(x)))
+
+    def antiquote_special(special: Symbol.Symbol => Boolean): Parser[Antiquote] =
+      many1(s => !special(s)) ^^ Text.apply |
+      one(special) ~ opt(cartouche) ^^
+        { case x ~ Some(y) => Control(x + y) case x ~ None => Control(x) }
   }