1.1 --- a/NEWS	Thu Mar 15 19:02:34 2012 +0100
     1.2 +++ b/NEWS	Thu Mar 15 19:48:19 2012 +0100
     1.3 @@ -371,6 +371,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Antiquotation @{keyword "name"} produces a parser for outer syntax
     1.8 +from a minor keyword introduced via theory header declaration.
     1.9 +
    1.10  * Local_Theory.define no longer hard-wires default theorem name
    1.11  "foo_def": definitional packages need to make this explicit, and may
    1.12  choose to omit theorem bindings for definitions by using

     2.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 15 19:02:34 2012 +0100
     2.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 15 19:48:19 2012 +0100
     2.3 @@ -182,5 +182,16 @@
     2.4            val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
     2.5          in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
     2.6  
     2.7 +
     2.8 +(* outer syntax *)
     2.9 +
    2.10 +val _ = Context.>> (Context.map_theory
    2.11 +  (value (Binding.name "keyword")
    2.12 +    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
    2.13 +      (if is_none (Thy_Header.the_keyword thy name) then
    2.14 +        ML_Syntax.atomic ("Parse.$$$ " ^ ML_Syntax.print_string name)
    2.15 +       else error ("Unknown minor keyword " ^ quote name))
    2.16 +      handle ERROR msg => error (msg ^ Position.str_of pos)))));
    2.17 +
    2.18  end;
    2.19