60 |
60 |
61 |
61 |
62 |
62 |
63 (** concrete antiquotations **) |
63 (** concrete antiquotations **) |
64 |
64 |
|
65 structure P = OuterParse; |
|
66 |
|
67 |
65 (* misc *) |
68 (* misc *) |
66 |
69 |
67 val _ = value "theory" |
70 val _ = value "theory" |
68 (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name) |
71 (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name) |
69 || Scan.succeed "ML_Context.the_global_context ()"); |
72 || Scan.succeed "ML_Context.the_global_context ()"); |
81 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
84 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
82 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
85 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
83 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
86 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
84 |
87 |
85 val _ = macro "let" (Args.context -- |
88 val _ = macro "let" (Args.context -- |
86 Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name)) |
89 Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name))) |
87 >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt))); |
90 >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt))); |
88 |
91 |
89 val _ = macro "note" (Args.context :|-- (fn ctxt => |
92 val _ = macro "note" (Args.context :|-- (fn ctxt => |
90 Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) => |
93 P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) => |
91 ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])]))) |
94 ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])]))) |
92 >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt)))); |
95 >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt)))); |
93 |
96 |
94 val _ = value "ctyp" (Args.typ >> (fn T => |
97 val _ = value "ctyp" (Args.typ >> (fn T => |
95 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))); |
98 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))); |
121 |
124 |
122 val _ = inline "const_name" (const false); |
125 val _ = inline "const_name" (const false); |
123 val _ = inline "const_syntax" (const true); |
126 val _ = inline "const_syntax" (const true); |
124 |
127 |
125 val _ = inline "const" |
128 val _ = inline "const" |
126 (Args.context -- Scan.lift Args.name -- |
129 (Args.context -- Scan.lift Args.name -- Scan.optional |
127 Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
130 (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
128 >> (fn ((ctxt, c), Ts) => |
131 >> (fn ((ctxt, c), Ts) => |
129 let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c) |
132 let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c) |
130 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
133 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
131 |
134 |
132 end; |
135 end; |