169 (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> |
169 (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> |
170 ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close> |
170 ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close> |
171 (const_name (fn (_, c) => Lexicon.mark_const c)) #> |
171 (const_name (fn (_, c) => Lexicon.mark_const c)) #> |
172 |
172 |
173 ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close> |
173 ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close> |
174 (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) => |
174 (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => |
175 if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) |
175 ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> |
176 then ML_Syntax.print_string c |
|
177 else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> |
|
178 |
176 |
179 ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close> |
177 ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close> |
180 (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional |
178 (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional |
181 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
179 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
182 >> (fn ((ctxt, (raw_c, pos)), Ts) => |
180 >> (fn ((ctxt, (raw_c, pos)), Ts) => |