# HG changeset patch
# User wenzelm
# Date 1214659048 -7200
# Node ID c706b72018262ade3fc0501d54f4f79647d620f3
# Parent  0968c0d0b96938d9648bbb82b4a0769304f6c1e6
added macro interface;
added @{let}, @{note};

diff -r 0968c0d0b969 -r c706b7201826 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Jun 28 15:17:26 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Jun 28 15:17:28 2008 +0200
@@ -7,6 +7,8 @@
 
 signature ML_ANTIQUOTE =
 sig
+  val macro: string ->
+    (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
   val variant: string -> Proof.context -> string * Proof.context
   val inline: string ->
     (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
@@ -41,8 +43,12 @@
 
 (* specific antiquotations *)
 
+fun macro name scan = ML_Context.add_antiq name
+  (scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
+    (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
+
 fun inline name scan = ML_Context.add_antiq name
-  (scan >> (fn s => fn {struct_name, background} => ((K ("", s)), background)));
+  (scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
 
 fun declaration kind name scan = ML_Context.add_antiq name
   (scan >> (fn s => fn {struct_name, background} =>
@@ -78,6 +84,15 @@
 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
 
+val _ = macro "let" (Args.context --
+  Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name))
+    >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
+
+val _ = macro "note" (Args.context :|-- (fn ctxt =>
+  Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
+    ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
+  >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
+
 val _ = value "ctyp" (Args.typ >> (fn T =>
   "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));