src/Pure/General/antiquote.ML
changeset 61476 1884c40f1539
parent 61475 5b58a17c440a
child 61481 078ec7b710ab
equal deleted inserted replaced
61475:5b58a17c440a 61476:1884c40f1539
    75 local
    75 local
    76 
    76 
    77 val err_prefix = "Antiquotation lexical error: ";
    77 val err_prefix = "Antiquotation lexical error: ";
    78 
    78 
    79 val scan_txt =
    79 val scan_txt =
    80   Scan.repeat1
    80   Scan.repeats1
    81    (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) ||
    81    (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) ||
    82     Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
    82     Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
    83     $$$ "@" --| Scan.ahead (~$$ "{")) >> flat;
    83     $$$ "@" --| Scan.ahead (~$$ "{"));
    84 
    84 
    85 val scan_antiq_body =
    85 val scan_antiq_body =
    86   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    86   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    87   Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
    87   Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
    88   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
    88   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
    99       in {name = (name, pos), range = range, body = body} end);
    99       in {name = (name, pos), range = range, body = body} end);
   100 
   100 
   101 val scan_antiq =
   101 val scan_antiq =
   102   Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
   102   Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
   103     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
   103     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
   104       (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
   104       (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
   105     (fn (pos1, (pos2, ((body, pos3), pos4))) =>
   105     (fn (pos1, (pos2, ((body, pos3), pos4))) =>
   106       {start = Position.set_range (pos1, pos2),
   106       {start = Position.set_range (pos1, pos2),
   107        stop = Position.set_range (pos3, pos4),
   107        stop = Position.set_range (pos3, pos4),
   108        range = Position.range pos1 pos4,
   108        range = Position.range pos1 pos4,
   109        body = flat body});
   109        body = body});
   110 
   110 
   111 val scan_antiquote =
   111 val scan_antiquote =
   112   scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;
   112   scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;
   113 
   113 
   114 end;
   114 end;