# HG changeset patch
# User wenzelm
# Date 1331837299 -3600
# Node ID aae5566d67562c1e40132bb381482a9eb0e525ef
# Parent  b8c7eb0c2f89fa6d1b43509ba1348dd8301fa393
added ML antiquotation @{keyword};

diff -r b8c7eb0c2f89 -r aae5566d6756 NEWS
--- a/NEWS	Thu Mar 15 19:02:34 2012 +0100
+++ b/NEWS	Thu Mar 15 19:48:19 2012 +0100
@@ -371,6 +371,9 @@
 
 *** ML ***
 
+* Antiquotation @{keyword "name"} produces a parser for outer syntax
+from a minor keyword introduced via theory header declaration.
+
 * Local_Theory.define no longer hard-wires default theorem name
 "foo_def": definitional packages need to make this explicit, and may
 choose to omit theorem bindings for definitions by using
diff -r b8c7eb0c2f89 -r aae5566d6756 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 15 19:02:34 2012 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 15 19:48:19 2012 +0100
@@ -182,5 +182,16 @@
           val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
         in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
 
+
+(* outer syntax *)
+
+val _ = Context.>> (Context.map_theory
+  (value (Binding.name "keyword")
+    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
+      (if is_none (Thy_Header.the_keyword thy name) then
+        ML_Syntax.atomic ("Parse.$$$ " ^ ML_Syntax.print_string name)
+       else error ("Unknown minor keyword " ^ quote name))
+      handle ERROR msg => error (msg ^ Position.str_of pos)))));
+
 end;