src/Pure/General/antiquote.ML
changeset 55046 9e83995c8e98
parent 53167 4e7ddd76e632
child 55105 75815b3b38a1
equal deleted inserted replaced
55045:99056d23e05b 55046:9e83995c8e98
    48   $$$ "@" --| Scan.ahead (~$$$ "{") ||
    48   $$$ "@" --| Scan.ahead (~$$$ "{") ||
    49   Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
    49   Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
    50 
    50 
    51 val scan_ant =
    51 val scan_ant =
    52   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    52   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
       
    53   Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 ||
    53   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    54   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    54 
    55 
    55 in
    56 in
    56 
    57 
    57 val scan_antiq =
    58 val scan_antiq =