clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
--- a/src/Pure/General/antiquote.ML Wed Feb 28 17:05:34 2018 +0100
+++ b/src/Pure/General/antiquote.ML Thu Mar 01 12:24:08 2018 +0100
@@ -102,6 +102,9 @@
val scan_antiq_body =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
Symbol_Pos.scan_cartouche err_prefix ||
+ Comment.scan --
+ Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
+ >> K [] ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name);