src/Pure/General/antiquote.ML
changeset 67735 e2e002d4a4de
parent 67571 f858fe5531ac
child 69592 a80d8ec6c998
equal deleted inserted replaced
67734:7b0b0a02b303 67735:e2e002d4a4de
   100   scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
   100   scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
   101 
   101 
   102 val scan_antiq_body =
   102 val scan_antiq_body =
   103   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   103   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   104   Symbol_Pos.scan_cartouche err_prefix ||
   104   Symbol_Pos.scan_cartouche err_prefix ||
       
   105   Comment.scan --
       
   106     Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
       
   107     >> K [] ||
   105   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
   108   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
   106 
   109 
   107 fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name);
   110 fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name);
   108 
   111 
   109 in
   112 in