clarified modules;
authorwenzelm
Tue Mar 18 16:16:28 2014 +0100 (2014-03-18)
changeset 56205ceb8a93460b7
parent 56204 f70e69208a8c
child 56206 7adec2a527f5
clarified modules;
more antiquotations for antiquotations;
NEWS
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Pure.thy
src/Pure/ROOT.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Tue Mar 18 15:29:58 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 18 16:16:28 2014 +0100
     1.3 @@ -465,10 +465,8 @@
     1.4  theory merge).  Note that the softer Thm.eq_thm_prop is often more
     1.5  appropriate than Thm.eq_thm.
     1.6  
     1.7 -* Simplified programming interface to define ML antiquotations (to
     1.8 -make it more close to the analogous Thy_Output.antiquotation).  See
     1.9 -ML_Context.antiquotation and structure ML_Antiquotation.  Minor
    1.10 -INCOMPATIBILITY.
    1.11 +* Simplified programming interface to define ML antiquotations, see
    1.12 +structure ML_Antiquotation.  Minor INCOMPATIBILITY.
    1.13  
    1.14  * ML antiquotation @{here} refers to its source position, which is
    1.15  occasionally useful for experimentation and diagnostic purposes.
     2.1 --- a/src/Pure/ML/ml_antiquotation.ML	Tue Mar 18 15:29:58 2014 +0100
     2.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Tue Mar 18 16:16:28 2014 +0100
     2.3 @@ -1,13 +1,15 @@
     2.4  (*  Title:      Pure/ML/ml_antiquotation.ML
     2.5      Author:     Makarius
     2.6  
     2.7 -Convenience operations for common ML antiquotations.  Miscellaneous
     2.8 -predefined antiquotations.
     2.9 +ML antiquotations.
    2.10  *)
    2.11  
    2.12  signature ML_ANTIQUOTATION =
    2.13  sig
    2.14    val variant: string -> Proof.context -> string * Proof.context
    2.15 +  val declaration: binding -> 'a context_parser ->
    2.16 +    (Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
    2.17 +    theory -> theory
    2.18    val inline: binding -> string context_parser -> theory -> theory
    2.19    val value: binding -> string context_parser -> theory -> theory
    2.20  end;
    2.21 @@ -15,9 +17,7 @@
    2.22  structure ML_Antiquotation: ML_ANTIQUOTATION =
    2.23  struct
    2.24  
    2.25 -(** generic tools **)
    2.26 -
    2.27 -(* ML names *)
    2.28 +(* unique names *)
    2.29  
    2.30  val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
    2.31  
    2.32 @@ -35,13 +35,19 @@
    2.33    in (b, ctxt') end;
    2.34  
    2.35  
    2.36 -(* specific antiquotations *)
    2.37 +(* define antiquotations *)
    2.38 +
    2.39 +fun declaration name scan body =
    2.40 +  ML_Context.add_antiquotation name
    2.41 +    (fn src => fn orig_ctxt =>
    2.42 +      let val (x, _) = Args.syntax scan src orig_ctxt
    2.43 +      in body src x orig_ctxt end);
    2.44  
    2.45  fun inline name scan =
    2.46 -  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    2.47 +  declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    2.48  
    2.49  fun value name scan =
    2.50 -  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
    2.51 +  declaration name scan (fn _ => fn s => fn ctxt =>
    2.52      let
    2.53        val (a, ctxt') = variant (Binding.name_of name) ctxt;
    2.54        val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    2.55 @@ -49,11 +55,10 @@
    2.56      in (K (env, body), ctxt') end);
    2.57  
    2.58  
    2.59 -
    2.60 -(** misc antiquotations **)
    2.61 +(* basic antiquotations *)
    2.62  
    2.63  val _ = Theory.setup
    2.64 - (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
    2.65 + (declaration (Binding.name "here") (Scan.succeed ())
    2.66      (fn src => fn () => fn ctxt =>
    2.67        let
    2.68          val (a, ctxt') = variant "position" ctxt;
    2.69 @@ -62,163 +67,8 @@
    2.70          val body = "Isabelle." ^ a;
    2.71        in (K (env, body), ctxt') end) #>
    2.72  
    2.73 -  inline (Binding.name "assert")
    2.74 -    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    2.75 -
    2.76 -  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
    2.77 -
    2.78 -  value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    2.79 -    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
    2.80 -     ML_Syntax.print_string name))) #>
    2.81 -
    2.82    value (Binding.name "binding")
    2.83 -    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
    2.84 -
    2.85 -  value (Binding.name "theory")
    2.86 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    2.87 -      (Context_Position.report ctxt pos
    2.88 -        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    2.89 -       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    2.90 -    || Scan.succeed "Proof_Context.theory_of ML_context") #>
    2.91 -
    2.92 -  value (Binding.name "theory_context")
    2.93 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    2.94 -      (Context_Position.report ctxt pos
    2.95 -        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    2.96 -       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    2.97 -        ML_Syntax.print_string name))) #>
    2.98 -
    2.99 -  inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
   2.100 -
   2.101 -  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   2.102 -  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   2.103 -  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   2.104 -
   2.105 -  value (Binding.name "ctyp") (Args.typ >> (fn T =>
   2.106 -    "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
   2.107 -      ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
   2.108 -
   2.109 -  value (Binding.name "cterm") (Args.term >> (fn t =>
   2.110 -    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   2.111 -     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   2.112 -
   2.113 -  value (Binding.name "cprop") (Args.prop >> (fn t =>
   2.114 -    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   2.115 -     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   2.116 -
   2.117 -  value (Binding.name "cpat")
   2.118 -    (Args.context --
   2.119 -      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   2.120 -        "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   2.121 -          ML_Syntax.atomic (ML_Syntax.print_term t))));
   2.122 -
   2.123 -
   2.124 -(* type classes *)
   2.125 -
   2.126 -fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   2.127 -  Proof_Context.read_class ctxt s
   2.128 -  |> syn ? Lexicon.mark_class
   2.129 -  |> ML_Syntax.print_string);
   2.130 -
   2.131 -val _ = Theory.setup
   2.132 - (inline (Binding.name "class") (class false) #>
   2.133 -  inline (Binding.name "class_syntax") (class true) #>
   2.134 -
   2.135 -  inline (Binding.name "sort")
   2.136 -    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   2.137 -      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   2.138 -
   2.139 -
   2.140 -(* type constructors *)
   2.141 -
   2.142 -fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   2.143 -  >> (fn (ctxt, (s, pos)) =>
   2.144 -    let
   2.145 -      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
   2.146 -      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   2.147 -      val res =
   2.148 -        (case try check (c, decl) of
   2.149 -          SOME res => res
   2.150 -        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
   2.151 -    in ML_Syntax.print_string res end);
   2.152 -
   2.153 -val _ = Theory.setup
   2.154 - (inline (Binding.name "type_name")
   2.155 -    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   2.156 -  inline (Binding.name "type_abbrev")
   2.157 -    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   2.158 -  inline (Binding.name "nonterminal")
   2.159 -    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   2.160 -  inline (Binding.name "type_syntax")
   2.161 -    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   2.162 -
   2.163 -
   2.164 -(* constants *)
   2.165 -
   2.166 -fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   2.167 -  >> (fn (ctxt, (s, pos)) =>
   2.168 -    let
   2.169 -      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
   2.170 -      val res = check (Proof_Context.consts_of ctxt, c)
   2.171 -        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   2.172 -    in ML_Syntax.print_string res end);
   2.173 -
   2.174 -val _ = Theory.setup
   2.175 - (inline (Binding.name "const_name")
   2.176 -    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   2.177 -  inline (Binding.name "const_abbrev")
   2.178 -    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   2.179 -  inline (Binding.name "const_syntax")
   2.180 -    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   2.181 -
   2.182 -  inline (Binding.name "syntax_const")
   2.183 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   2.184 -      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   2.185 -      then ML_Syntax.print_string c
   2.186 -      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   2.187 -
   2.188 -  inline (Binding.name "const")
   2.189 -    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
   2.190 -        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   2.191 -      >> (fn ((ctxt, raw_c), Ts) =>
   2.192 -        let
   2.193 -          val Const (c, _) =
   2.194 -            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
   2.195 -          val consts = Proof_Context.consts_of ctxt;
   2.196 -          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   2.197 -          val _ = length Ts <> n andalso
   2.198 -            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
   2.199 -              quote c ^ enclose "(" ")" (commas (replicate n "_")));
   2.200 -          val const = Const (c, Consts.instance consts (c, Ts));
   2.201 -        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
   2.202 -
   2.203 -
   2.204 -(* outer syntax *)
   2.205 -
   2.206 -fun with_keyword f =
   2.207 -  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
   2.208 -    (f ((name, Thy_Header.the_keyword thy name), pos)
   2.209 -      handle ERROR msg => error (msg ^ Position.here pos)));
   2.210 -
   2.211 -val _ = Theory.setup
   2.212 - (value (Binding.name "keyword")
   2.213 -    (with_keyword
   2.214 -      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   2.215 -        | ((name, SOME _), pos) =>
   2.216 -            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   2.217 -  value (Binding.name "command_spec")
   2.218 -    (with_keyword
   2.219 -      (fn ((name, SOME kind), pos) =>
   2.220 -          "Keyword.command_spec " ^ ML_Syntax.atomic
   2.221 -            ((ML_Syntax.print_pair
   2.222 -              (ML_Syntax.print_pair ML_Syntax.print_string
   2.223 -                (ML_Syntax.print_pair
   2.224 -                  (ML_Syntax.print_pair ML_Syntax.print_string
   2.225 -                    (ML_Syntax.print_list ML_Syntax.print_string))
   2.226 -                  (ML_Syntax.print_list ML_Syntax.print_string)))
   2.227 -              ML_Syntax.print_position) ((name, kind), pos))
   2.228 -        | ((name, NONE), pos) =>
   2.229 -            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   2.230 +    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
   2.231  
   2.232  end;
   2.233  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Tue Mar 18 16:16:28 2014 +0100
     3.3 @@ -0,0 +1,167 @@
     3.4 +(*  Title:      Pure/ML/ml_antiquotations.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Miscellaneous ML antiquotations.
     3.8 +*)
     3.9 +
    3.10 +structure ML_Antiquotations: sig end =
    3.11 +struct
    3.12 +
    3.13 +val _ = Theory.setup
    3.14 + (ML_Antiquotation.inline @{binding assert}
    3.15 +    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    3.16 +
    3.17 +  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
    3.18 +
    3.19 +  ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    3.20 +    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
    3.21 +     ML_Syntax.print_string name))) #>
    3.22 +
    3.23 +  ML_Antiquotation.value @{binding theory}
    3.24 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    3.25 +      (Context_Position.report ctxt pos
    3.26 +        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    3.27 +       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    3.28 +    || Scan.succeed "Proof_Context.theory_of ML_context") #>
    3.29 +
    3.30 +  ML_Antiquotation.value @{binding theory_context}
    3.31 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    3.32 +      (Context_Position.report ctxt pos
    3.33 +        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    3.34 +       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    3.35 +        ML_Syntax.print_string name))) #>
    3.36 +
    3.37 +  ML_Antiquotation.inline @{binding context} (Scan.succeed "Isabelle.ML_context") #>
    3.38 +
    3.39 +  ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    3.40 +  ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    3.41 +  ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    3.42 +
    3.43 +  ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
    3.44 +    "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
    3.45 +      ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
    3.46 +
    3.47 +  ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
    3.48 +    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    3.49 +     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    3.50 +
    3.51 +  ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
    3.52 +    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    3.53 +     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    3.54 +
    3.55 +  ML_Antiquotation.value @{binding cpat}
    3.56 +    (Args.context --
    3.57 +      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
    3.58 +        "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    3.59 +          ML_Syntax.atomic (ML_Syntax.print_term t))));
    3.60 +
    3.61 +
    3.62 +(* type classes *)
    3.63 +
    3.64 +fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
    3.65 +  Proof_Context.read_class ctxt s
    3.66 +  |> syn ? Lexicon.mark_class
    3.67 +  |> ML_Syntax.print_string);
    3.68 +
    3.69 +val _ = Theory.setup
    3.70 + (ML_Antiquotation.inline @{binding class} (class false) #>
    3.71 +  ML_Antiquotation.inline @{binding class_syntax} (class true) #>
    3.72 +
    3.73 +  ML_Antiquotation.inline @{binding sort}
    3.74 +    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
    3.75 +      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
    3.76 +
    3.77 +
    3.78 +(* type constructors *)
    3.79 +
    3.80 +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
    3.81 +  >> (fn (ctxt, (s, pos)) =>
    3.82 +    let
    3.83 +      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
    3.84 +      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
    3.85 +      val res =
    3.86 +        (case try check (c, decl) of
    3.87 +          SOME res => res
    3.88 +        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
    3.89 +    in ML_Syntax.print_string res end);
    3.90 +
    3.91 +val _ = Theory.setup
    3.92 + (ML_Antiquotation.inline @{binding type_name}
    3.93 +    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
    3.94 +  ML_Antiquotation.inline @{binding type_abbrev}
    3.95 +    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
    3.96 +  ML_Antiquotation.inline @{binding nonterminal}
    3.97 +    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
    3.98 +  ML_Antiquotation.inline @{binding type_syntax}
    3.99 +    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   3.100 +
   3.101 +
   3.102 +(* constants *)
   3.103 +
   3.104 +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   3.105 +  >> (fn (ctxt, (s, pos)) =>
   3.106 +    let
   3.107 +      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
   3.108 +      val res = check (Proof_Context.consts_of ctxt, c)
   3.109 +        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   3.110 +    in ML_Syntax.print_string res end);
   3.111 +
   3.112 +val _ = Theory.setup
   3.113 + (ML_Antiquotation.inline @{binding const_name}
   3.114 +    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   3.115 +  ML_Antiquotation.inline @{binding const_abbrev}
   3.116 +    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   3.117 +  ML_Antiquotation.inline @{binding const_syntax}
   3.118 +    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   3.119 +
   3.120 +  ML_Antiquotation.inline @{binding syntax_const}
   3.121 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   3.122 +      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   3.123 +      then ML_Syntax.print_string c
   3.124 +      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   3.125 +
   3.126 +  ML_Antiquotation.inline @{binding const}
   3.127 +    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
   3.128 +        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   3.129 +      >> (fn ((ctxt, raw_c), Ts) =>
   3.130 +        let
   3.131 +          val Const (c, _) =
   3.132 +            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
   3.133 +          val consts = Proof_Context.consts_of ctxt;
   3.134 +          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   3.135 +          val _ = length Ts <> n andalso
   3.136 +            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
   3.137 +              quote c ^ enclose "(" ")" (commas (replicate n "_")));
   3.138 +          val const = Const (c, Consts.instance consts (c, Ts));
   3.139 +        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
   3.140 +
   3.141 +
   3.142 +(* outer syntax *)
   3.143 +
   3.144 +fun with_keyword f =
   3.145 +  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
   3.146 +    (f ((name, Thy_Header.the_keyword thy name), pos)
   3.147 +      handle ERROR msg => error (msg ^ Position.here pos)));
   3.148 +
   3.149 +val _ = Theory.setup
   3.150 + (ML_Antiquotation.value @{binding keyword}
   3.151 +    (with_keyword
   3.152 +      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   3.153 +        | ((name, SOME _), pos) =>
   3.154 +            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   3.155 +  ML_Antiquotation.value @{binding command_spec}
   3.156 +    (with_keyword
   3.157 +      (fn ((name, SOME kind), pos) =>
   3.158 +          "Keyword.command_spec " ^ ML_Syntax.atomic
   3.159 +            ((ML_Syntax.print_pair
   3.160 +              (ML_Syntax.print_pair ML_Syntax.print_string
   3.161 +                (ML_Syntax.print_pair
   3.162 +                  (ML_Syntax.print_pair ML_Syntax.print_string
   3.163 +                    (ML_Syntax.print_list ML_Syntax.print_string))
   3.164 +                  (ML_Syntax.print_list ML_Syntax.print_string)))
   3.165 +              ML_Syntax.print_position) ((name, kind), pos))
   3.166 +        | ((name, NONE), pos) =>
   3.167 +            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   3.168 +
   3.169 +end;
   3.170 +
     4.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 18 15:29:58 2014 +0100
     4.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 18 16:16:28 2014 +0100
     4.3 @@ -13,10 +13,10 @@
     4.4    val thms: xstring -> thm list
     4.5    val exec: (unit -> unit) -> Context.generic -> Context.generic
     4.6    val check_antiquotation: Proof.context -> xstring * Position.T -> string
     4.7 +  type decl = Proof.context -> string * string
     4.8 +  val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
     4.9 +    theory -> theory
    4.10    val print_antiquotations: Proof.context -> unit
    4.11 -  type decl = Proof.context -> string * string
    4.12 -  val antiquotation: binding -> 'a context_parser ->
    4.13 -    (Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory
    4.14    val trace_raw: Config.raw
    4.15    val trace: bool Config.T
    4.16    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    4.17 @@ -80,12 +80,6 @@
    4.18    let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
    4.19    in f src' ctxt end;
    4.20  
    4.21 -fun antiquotation name scan body =
    4.22 -  add_antiquotation name
    4.23 -    (fn src => fn orig_ctxt =>
    4.24 -      let val (x, _) = Args.syntax scan src orig_ctxt
    4.25 -      in body src x orig_ctxt end);
    4.26 -
    4.27  
    4.28  (* parsing and evaluation *)
    4.29  
     5.1 --- a/src/Pure/ML/ml_thms.ML	Tue Mar 18 15:29:58 2014 +0100
     5.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Mar 18 16:16:28 2014 +0100
     5.3 @@ -41,7 +41,7 @@
     5.4  (* attribute source *)
     5.5  
     5.6  val _ = Theory.setup
     5.7 -  (ML_Context.antiquotation @{binding attributes} (Scan.lift Parse_Spec.attribs)
     5.8 +  (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse_Spec.attribs)
     5.9      (fn _ => fn raw_srcs => fn ctxt =>
    5.10        let
    5.11          val i = serial ();
    5.12 @@ -74,8 +74,8 @@
    5.13    in (decl, ctxt'') end;
    5.14  
    5.15  val _ = Theory.setup
    5.16 -  (ML_Context.antiquotation @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
    5.17 -   ML_Context.antiquotation @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
    5.18 +  (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
    5.19 +   ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
    5.20  
    5.21  
    5.22  (* ad-hoc goals *)
    5.23 @@ -85,7 +85,7 @@
    5.24  val goal = Scan.unless (by || and_) Args.name_inner_syntax;
    5.25  
    5.26  val _ = Theory.setup
    5.27 -  (ML_Context.antiquotation @{binding lemma}
    5.28 +  (ML_Antiquotation.declaration @{binding lemma}
    5.29      (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
    5.30        (by |-- Method.parse -- Scan.option Method.parse)))
    5.31      (fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
     6.1 --- a/src/Pure/Pure.thy	Tue Mar 18 15:29:58 2014 +0100
     6.2 +++ b/src/Pure/Pure.thy	Tue Mar 18 16:16:28 2014 +0100
     6.3 @@ -103,6 +103,7 @@
     6.4      "ProofGeneral.inform_file_retracted" :: control
     6.5  begin
     6.6  
     6.7 +ML_file "ML/ml_antiquotations.ML"
     6.8  ML_file "ML/ml_thms.ML"
     6.9  ML_file "Isar/isar_syn.ML"
    6.10  ML_file "Isar/calculation.ML"
     7.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 15:29:58 2014 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 16:16:28 2014 +0100
     7.3 @@ -231,13 +231,13 @@
     7.4  
     7.5  (*ML with context and antiquotations*)
     7.6  use "ML/ml_context.ML";
     7.7 +use "ML/ml_antiquotation.ML";
     7.8  val use = ML_Context.eval_file true o Path.explode;
     7.9  (*^^^^^ end of ML bootstrap 1 ^^^^^*)
    7.10  
    7.11  (*basic proof engine*)
    7.12  use "Isar/proof_display.ML";
    7.13  use "Isar/attrib.ML";
    7.14 -use "ML/ml_antiquotation.ML";
    7.15  use "Isar/context_rules.ML";
    7.16  use "Isar/method.ML";
    7.17  use "Isar/proof.ML";
     8.1 --- a/src/Tools/Code/code_runtime.ML	Tue Mar 18 15:29:58 2014 +0100
     8.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Mar 18 16:16:28 2014 +0100
     8.3 @@ -354,7 +354,7 @@
     8.4  (** Isar setup **)
     8.5  
     8.6  val _ =
     8.7 -  Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq));
     8.8 +  Theory.setup (ML_Antiquotation.declaration @{binding code} Args.term (fn _ => ml_code_antiq));
     8.9  
    8.10  local
    8.11