--- 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) }
}