clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
authorwenzelm
Thu, 01 Mar 2018 12:24:08 +0100
changeset 67735 e2e002d4a4de
parent 67734 7b0b0a02b303
child 67736 65016740d3e0
clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
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);