diff -r 7b0b0a02b303 -r e2e002d4a4de src/Pure/General/antiquote.ML --- 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);