equal
deleted
inserted
replaced
68 |
68 |
69 |
69 |
70 (* ML macros *) |
70 (* ML macros *) |
71 |
71 |
72 fun special_form binding parse = |
72 fun special_form binding parse = |
73 ML_Context.add_antiquotation binding true |
73 ML_Context.add_antiquotation_embedded binding |
74 (fn _ => fn src => fn ctxt => |
74 (fn _ => fn input => fn ctxt => |
75 let |
75 let |
76 val input = Token.read ctxt Parse.embedded_input src; |
|
77 val tokenize = ML_Lex.tokenize_no_range; |
76 val tokenize = ML_Lex.tokenize_no_range; |
78 val tokenize_range = ML_Lex.tokenize_range (Input.range_of input); |
77 val tokenize_range = ML_Lex.tokenize_range (Input.range_of input); |
79 val eq = tokenize " = "; |
78 val eq = tokenize " = "; |
80 |
79 |
81 val (operator, sections) = parse ctxt input; |
80 val (operator, sections) = parse ctxt input; |
95 tokenize operator @ maps #2 sections_bind @ tokenize " in result end"; |
94 tokenize operator @ maps #2 sections_bind @ tokenize " in result end"; |
96 in (flat sections_env, ml_body') end; |
95 in (flat sections_env, ml_body') end; |
97 in (decl', ctxt') end); |
96 in (decl', ctxt') end); |
98 |
97 |
99 fun conditional binding check = |
98 fun conditional binding check = |
100 ML_Context.add_antiquotation binding true |
99 ML_Context.add_antiquotation_embedded binding |
101 (fn _ => fn src => fn ctxt => |
100 (fn _ => fn input => fn ctxt => |
102 let val s = Token.read ctxt Parse.embedded_input src in |
101 if check ctxt then ML_Context.read_antiquotes input ctxt |
103 if check ctxt then ML_Context.read_antiquotes s ctxt |
102 else (K ([], []), ctxt)); |
104 else (K ([], []), ctxt) |
|
105 end); |
|
106 |
103 |
107 |
104 |
108 (* basic antiquotations *) |
105 (* basic antiquotations *) |
109 |
106 |
110 val _ = Theory.setup |
107 val _ = Theory.setup |