tuned signature -- clarified module name;
authorwenzelm
Wed Mar 12 22:57:50 2014 +0100 (2014-03-12 ago)
changeset 5607231e427387ab5
parent 56071 2ffdedb0c044
child 56073 29e308b56d23
child 56134 4a7a07c01857
tuned signature -- clarified module name;
NEWS
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_thms.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/simplifier.ML
     1.1 --- a/NEWS	Wed Mar 12 22:44:55 2014 +0100
     1.2 +++ b/NEWS	Wed Mar 12 22:57:50 2014 +0100
     1.3 @@ -437,9 +437,10 @@
     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, see
     1.8 -ML_Context.antiquotation, to make it more close to the analogous
     1.9 -Thy_Output.antiquotation.  Minor INCOMPATIBILTY.
    1.10 +* Simplified programming interface to define ML antiquotations (to
    1.11 +make it more close to the analogous Thy_Output.antiquotation).  See
    1.12 +ML_Context.antiquotation and structure ML_Antiquotation.  Minor
    1.13 +INCOMPATIBILITY.
    1.14  
    1.15  * ML antiquotation @{here} refers to its source position, which is
    1.16  occasionally useful for experimentation and diagnostic purposes.
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Mar 12 22:44:55 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Mar 12 22:57:50 2014 +0100
     2.3 @@ -106,7 +106,7 @@
     2.4  
     2.5  setup -- "ML antiquotation"
     2.6  {*
     2.7 -  ML_Antiquote.inline @{binding term_cartouche}
     2.8 +  ML_Antiquotation.inline @{binding term_cartouche}
     2.9      (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
    2.10        (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
    2.11  *}
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 12 22:44:55 2014 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 12 22:57:50 2014 +0100
     3.3 @@ -247,9 +247,9 @@
     3.4      handle Toplevel.UNDEF => error "No goal present";
     3.5  
     3.6  val _ = Theory.setup
     3.7 -  (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
     3.8 +  (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
     3.9      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    3.10 -   ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    3.11 +   ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
    3.12      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    3.13  
    3.14  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Wed Mar 12 22:57:50 2014 +0100
     4.3 @@ -0,0 +1,224 @@
     4.4 +(*  Title:      Pure/ML/ml_antiquotation.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Convenience operations for common ML antiquotations.  Miscellaneous
     4.8 +predefined antiquotations.
     4.9 +*)
    4.10 +
    4.11 +signature ML_ANTIQUOTATION =
    4.12 +sig
    4.13 +  val variant: string -> Proof.context -> string * Proof.context
    4.14 +  val inline: binding -> string context_parser -> theory -> theory
    4.15 +  val value: binding -> string context_parser -> theory -> theory
    4.16 +end;
    4.17 +
    4.18 +structure ML_Antiquotation: ML_ANTIQUOTATION =
    4.19 +struct
    4.20 +
    4.21 +(** generic tools **)
    4.22 +
    4.23 +(* ML names *)
    4.24 +
    4.25 +val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
    4.26 +
    4.27 +structure Names = Proof_Data
    4.28 +(
    4.29 +  type T = Name.context;
    4.30 +  fun init _ = init_context;
    4.31 +);
    4.32 +
    4.33 +fun variant a ctxt =
    4.34 +  let
    4.35 +    val names = Names.get ctxt;
    4.36 +    val (b, names') = Name.variant (Name.desymbolize false a) names;
    4.37 +    val ctxt' = Names.put names' ctxt;
    4.38 +  in (b, ctxt') end;
    4.39 +
    4.40 +
    4.41 +(* specific antiquotations *)
    4.42 +
    4.43 +fun inline name scan =
    4.44 +  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    4.45 +
    4.46 +fun value name scan =
    4.47 +  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
    4.48 +    let
    4.49 +      val (a, ctxt') = variant (Binding.name_of name) ctxt;
    4.50 +      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    4.51 +      val body = "Isabelle." ^ a;
    4.52 +    in (K (env, body), ctxt') end);
    4.53 +
    4.54 +
    4.55 +
    4.56 +(** misc antiquotations **)
    4.57 +
    4.58 +val _ = Theory.setup
    4.59 + (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
    4.60 +    (fn src => fn () => fn ctxt =>
    4.61 +      let
    4.62 +        val (a, ctxt') = variant "position" ctxt;
    4.63 +        val (_, pos) = Args.name_of_src src;
    4.64 +        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
    4.65 +        val body = "Isabelle." ^ a;
    4.66 +      in (K (env, body), ctxt') end) #>
    4.67 +
    4.68 +  inline (Binding.name "assert")
    4.69 +    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    4.70 +
    4.71 +  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
    4.72 +
    4.73 +  value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    4.74 +    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
    4.75 +     ML_Syntax.print_string name))) #>
    4.76 +
    4.77 +  value (Binding.name "binding")
    4.78 +    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
    4.79 +
    4.80 +  value (Binding.name "theory")
    4.81 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    4.82 +      (Context_Position.report ctxt pos
    4.83 +        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    4.84 +       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    4.85 +    || Scan.succeed "Proof_Context.theory_of ML_context") #>
    4.86 +
    4.87 +  value (Binding.name "theory_context")
    4.88 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    4.89 +      (Context_Position.report ctxt pos
    4.90 +        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    4.91 +       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    4.92 +        ML_Syntax.print_string name))) #>
    4.93 +
    4.94 +  inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
    4.95 +
    4.96 +  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    4.97 +  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    4.98 +  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    4.99 +
   4.100 +  value (Binding.name "ctyp") (Args.typ >> (fn T =>
   4.101 +    "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
   4.102 +      ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
   4.103 +
   4.104 +  value (Binding.name "cterm") (Args.term >> (fn t =>
   4.105 +    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   4.106 +     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   4.107 +
   4.108 +  value (Binding.name "cprop") (Args.prop >> (fn t =>
   4.109 +    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   4.110 +     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   4.111 +
   4.112 +  value (Binding.name "cpat")
   4.113 +    (Args.context --
   4.114 +      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   4.115 +        "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   4.116 +          ML_Syntax.atomic (ML_Syntax.print_term t))));
   4.117 +
   4.118 +
   4.119 +(* type classes *)
   4.120 +
   4.121 +fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   4.122 +  Proof_Context.read_class ctxt s
   4.123 +  |> syn ? Lexicon.mark_class
   4.124 +  |> ML_Syntax.print_string);
   4.125 +
   4.126 +val _ = Theory.setup
   4.127 + (inline (Binding.name "class") (class false) #>
   4.128 +  inline (Binding.name "class_syntax") (class true) #>
   4.129 +
   4.130 +  inline (Binding.name "sort")
   4.131 +    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   4.132 +      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   4.133 +
   4.134 +
   4.135 +(* type constructors *)
   4.136 +
   4.137 +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   4.138 +  >> (fn (ctxt, (s, pos)) =>
   4.139 +    let
   4.140 +      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
   4.141 +      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   4.142 +      val res =
   4.143 +        (case try check (c, decl) of
   4.144 +          SOME res => res
   4.145 +        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
   4.146 +    in ML_Syntax.print_string res end);
   4.147 +
   4.148 +val _ = Theory.setup
   4.149 + (inline (Binding.name "type_name")
   4.150 +    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   4.151 +  inline (Binding.name "type_abbrev")
   4.152 +    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   4.153 +  inline (Binding.name "nonterminal")
   4.154 +    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   4.155 +  inline (Binding.name "type_syntax")
   4.156 +    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   4.157 +
   4.158 +
   4.159 +(* constants *)
   4.160 +
   4.161 +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   4.162 +  >> (fn (ctxt, (s, pos)) =>
   4.163 +    let
   4.164 +      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
   4.165 +      val res = check (Proof_Context.consts_of ctxt, c)
   4.166 +        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   4.167 +    in ML_Syntax.print_string res end);
   4.168 +
   4.169 +val _ = Theory.setup
   4.170 + (inline (Binding.name "const_name")
   4.171 +    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   4.172 +  inline (Binding.name "const_abbrev")
   4.173 +    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   4.174 +  inline (Binding.name "const_syntax")
   4.175 +    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   4.176 +
   4.177 +  inline (Binding.name "syntax_const")
   4.178 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   4.179 +      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   4.180 +      then ML_Syntax.print_string c
   4.181 +      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   4.182 +
   4.183 +  inline (Binding.name "const")
   4.184 +    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
   4.185 +        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   4.186 +      >> (fn ((ctxt, raw_c), Ts) =>
   4.187 +        let
   4.188 +          val Const (c, _) =
   4.189 +            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
   4.190 +          val consts = Proof_Context.consts_of ctxt;
   4.191 +          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   4.192 +          val _ = length Ts <> n andalso
   4.193 +            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
   4.194 +              quote c ^ enclose "(" ")" (commas (replicate n "_")));
   4.195 +          val const = Const (c, Consts.instance consts (c, Ts));
   4.196 +        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
   4.197 +
   4.198 +
   4.199 +(* outer syntax *)
   4.200 +
   4.201 +fun with_keyword f =
   4.202 +  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
   4.203 +    (f ((name, Thy_Header.the_keyword thy name), pos)
   4.204 +      handle ERROR msg => error (msg ^ Position.here pos)));
   4.205 +
   4.206 +val _ = Theory.setup
   4.207 + (value (Binding.name "keyword")
   4.208 +    (with_keyword
   4.209 +      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   4.210 +        | ((name, SOME _), pos) =>
   4.211 +            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   4.212 +  value (Binding.name "command_spec")
   4.213 +    (with_keyword
   4.214 +      (fn ((name, SOME kind), pos) =>
   4.215 +          "Keyword.command_spec " ^ ML_Syntax.atomic
   4.216 +            ((ML_Syntax.print_pair
   4.217 +              (ML_Syntax.print_pair ML_Syntax.print_string
   4.218 +                (ML_Syntax.print_pair
   4.219 +                  (ML_Syntax.print_pair ML_Syntax.print_string
   4.220 +                    (ML_Syntax.print_list ML_Syntax.print_string))
   4.221 +                  (ML_Syntax.print_list ML_Syntax.print_string)))
   4.222 +              ML_Syntax.print_position) ((name, kind), pos))
   4.223 +        | ((name, NONE), pos) =>
   4.224 +            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   4.225 +
   4.226 +end;
   4.227 +
     5.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:44:55 2014 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,223 +0,0 @@
     5.4 -(*  Title:      Pure/ML/ml_antiquote.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Common ML antiquotations.
     5.8 -*)
     5.9 -
    5.10 -signature ML_ANTIQUOTE =
    5.11 -sig
    5.12 -  val variant: string -> Proof.context -> string * Proof.context
    5.13 -  val inline: binding -> string context_parser -> theory -> theory
    5.14 -  val value: binding -> string context_parser -> theory -> theory
    5.15 -end;
    5.16 -
    5.17 -structure ML_Antiquote: ML_ANTIQUOTE =
    5.18 -struct
    5.19 -
    5.20 -(** generic tools **)
    5.21 -
    5.22 -(* ML names *)
    5.23 -
    5.24 -val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
    5.25 -
    5.26 -structure Names = Proof_Data
    5.27 -(
    5.28 -  type T = Name.context;
    5.29 -  fun init _ = init_context;
    5.30 -);
    5.31 -
    5.32 -fun variant a ctxt =
    5.33 -  let
    5.34 -    val names = Names.get ctxt;
    5.35 -    val (b, names') = Name.variant (Name.desymbolize false a) names;
    5.36 -    val ctxt' = Names.put names' ctxt;
    5.37 -  in (b, ctxt') end;
    5.38 -
    5.39 -
    5.40 -(* specific antiquotations *)
    5.41 -
    5.42 -fun inline name scan =
    5.43 -  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    5.44 -
    5.45 -fun value name scan =
    5.46 -  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
    5.47 -    let
    5.48 -      val (a, ctxt') = variant (Binding.name_of name) ctxt;
    5.49 -      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    5.50 -      val body = "Isabelle." ^ a;
    5.51 -    in (K (env, body), ctxt') end);
    5.52 -
    5.53 -
    5.54 -
    5.55 -(** misc antiquotations **)
    5.56 -
    5.57 -val _ = Theory.setup
    5.58 - (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
    5.59 -    (fn src => fn () => fn ctxt =>
    5.60 -      let
    5.61 -        val (a, ctxt') = variant "position" ctxt;
    5.62 -        val (_, pos) = Args.name_of_src src;
    5.63 -        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
    5.64 -        val body = "Isabelle." ^ a;
    5.65 -      in (K (env, body), ctxt') end) #>
    5.66 -
    5.67 -  inline (Binding.name "assert")
    5.68 -    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    5.69 -
    5.70 -  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
    5.71 -
    5.72 -  value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    5.73 -    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
    5.74 -     ML_Syntax.print_string name))) #>
    5.75 -
    5.76 -  value (Binding.name "binding")
    5.77 -    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
    5.78 -
    5.79 -  value (Binding.name "theory")
    5.80 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    5.81 -      (Context_Position.report ctxt pos
    5.82 -        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    5.83 -       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    5.84 -    || Scan.succeed "Proof_Context.theory_of ML_context") #>
    5.85 -
    5.86 -  value (Binding.name "theory_context")
    5.87 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    5.88 -      (Context_Position.report ctxt pos
    5.89 -        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    5.90 -       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    5.91 -        ML_Syntax.print_string name))) #>
    5.92 -
    5.93 -  inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
    5.94 -
    5.95 -  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    5.96 -  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    5.97 -  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    5.98 -
    5.99 -  value (Binding.name "ctyp") (Args.typ >> (fn T =>
   5.100 -    "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
   5.101 -      ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
   5.102 -
   5.103 -  value (Binding.name "cterm") (Args.term >> (fn t =>
   5.104 -    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   5.105 -     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   5.106 -
   5.107 -  value (Binding.name "cprop") (Args.prop >> (fn t =>
   5.108 -    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   5.109 -     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   5.110 -
   5.111 -  value (Binding.name "cpat")
   5.112 -    (Args.context --
   5.113 -      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   5.114 -        "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   5.115 -          ML_Syntax.atomic (ML_Syntax.print_term t))));
   5.116 -
   5.117 -
   5.118 -(* type classes *)
   5.119 -
   5.120 -fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   5.121 -  Proof_Context.read_class ctxt s
   5.122 -  |> syn ? Lexicon.mark_class
   5.123 -  |> ML_Syntax.print_string);
   5.124 -
   5.125 -val _ = Theory.setup
   5.126 - (inline (Binding.name "class") (class false) #>
   5.127 -  inline (Binding.name "class_syntax") (class true) #>
   5.128 -
   5.129 -  inline (Binding.name "sort")
   5.130 -    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   5.131 -      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   5.132 -
   5.133 -
   5.134 -(* type constructors *)
   5.135 -
   5.136 -fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   5.137 -  >> (fn (ctxt, (s, pos)) =>
   5.138 -    let
   5.139 -      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
   5.140 -      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   5.141 -      val res =
   5.142 -        (case try check (c, decl) of
   5.143 -          SOME res => res
   5.144 -        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
   5.145 -    in ML_Syntax.print_string res end);
   5.146 -
   5.147 -val _ = Theory.setup
   5.148 - (inline (Binding.name "type_name")
   5.149 -    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   5.150 -  inline (Binding.name "type_abbrev")
   5.151 -    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   5.152 -  inline (Binding.name "nonterminal")
   5.153 -    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   5.154 -  inline (Binding.name "type_syntax")
   5.155 -    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   5.156 -
   5.157 -
   5.158 -(* constants *)
   5.159 -
   5.160 -fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   5.161 -  >> (fn (ctxt, (s, pos)) =>
   5.162 -    let
   5.163 -      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
   5.164 -      val res = check (Proof_Context.consts_of ctxt, c)
   5.165 -        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   5.166 -    in ML_Syntax.print_string res end);
   5.167 -
   5.168 -val _ = Theory.setup
   5.169 - (inline (Binding.name "const_name")
   5.170 -    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   5.171 -  inline (Binding.name "const_abbrev")
   5.172 -    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   5.173 -  inline (Binding.name "const_syntax")
   5.174 -    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   5.175 -
   5.176 -  inline (Binding.name "syntax_const")
   5.177 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   5.178 -      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   5.179 -      then ML_Syntax.print_string c
   5.180 -      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   5.181 -
   5.182 -  inline (Binding.name "const")
   5.183 -    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
   5.184 -        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   5.185 -      >> (fn ((ctxt, raw_c), Ts) =>
   5.186 -        let
   5.187 -          val Const (c, _) =
   5.188 -            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
   5.189 -          val consts = Proof_Context.consts_of ctxt;
   5.190 -          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   5.191 -          val _ = length Ts <> n andalso
   5.192 -            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
   5.193 -              quote c ^ enclose "(" ")" (commas (replicate n "_")));
   5.194 -          val const = Const (c, Consts.instance consts (c, Ts));
   5.195 -        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
   5.196 -
   5.197 -
   5.198 -(* outer syntax *)
   5.199 -
   5.200 -fun with_keyword f =
   5.201 -  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
   5.202 -    (f ((name, Thy_Header.the_keyword thy name), pos)
   5.203 -      handle ERROR msg => error (msg ^ Position.here pos)));
   5.204 -
   5.205 -val _ = Theory.setup
   5.206 - (value (Binding.name "keyword")
   5.207 -    (with_keyword
   5.208 -      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   5.209 -        | ((name, SOME _), pos) =>
   5.210 -            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   5.211 -  value (Binding.name "command_spec")
   5.212 -    (with_keyword
   5.213 -      (fn ((name, SOME kind), pos) =>
   5.214 -          "Keyword.command_spec " ^ ML_Syntax.atomic
   5.215 -            ((ML_Syntax.print_pair
   5.216 -              (ML_Syntax.print_pair ML_Syntax.print_string
   5.217 -                (ML_Syntax.print_pair
   5.218 -                  (ML_Syntax.print_pair ML_Syntax.print_string
   5.219 -                    (ML_Syntax.print_list ML_Syntax.print_string))
   5.220 -                  (ML_Syntax.print_list ML_Syntax.print_string)))
   5.221 -              ML_Syntax.print_position) ((name, kind), pos))
   5.222 -        | ((name, NONE), pos) =>
   5.223 -            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   5.224 -
   5.225 -end;
   5.226 -
     6.1 --- a/src/Pure/ML/ml_thms.ML	Wed Mar 12 22:44:55 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Mar 12 22:57:50 2014 +0100
     6.3 @@ -42,7 +42,7 @@
     6.4          val srcs = map (Attrib.check_src ctxt) raw_srcs;
     6.5          val _ = map (Attrib.attribute ctxt) srcs;
     6.6          val (a, ctxt') = ctxt
     6.7 -          |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
     6.8 +          |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs);
     6.9          val ml =
    6.10            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
    6.11              string_of_int i ^ ";\n", "Isabelle." ^ a);
    6.12 @@ -54,7 +54,7 @@
    6.13  fun thm_binding kind is_single thms ctxt =
    6.14    let
    6.15      val initial = null (get_thmss ctxt);
    6.16 -    val (name, ctxt') = ML_Antiquote.variant kind ctxt;
    6.17 +    val (name, ctxt') = ML_Antiquotation.variant kind ctxt;
    6.18      val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
    6.19  
    6.20      val ml_body = "Isabelle." ^ name;
     7.1 --- a/src/Pure/ROOT	Wed Mar 12 22:44:55 2014 +0100
     7.2 +++ b/src/Pure/ROOT	Wed Mar 12 22:57:50 2014 +0100
     7.3 @@ -143,7 +143,7 @@
     7.4      "ML/exn_properties_polyml.ML"
     7.5      "ML/exn_trace_polyml-5.5.1.ML"
     7.6      "ML/install_pp_polyml.ML"
     7.7 -    "ML/ml_antiquote.ML"
     7.8 +    "ML/ml_antiquotation.ML"
     7.9      "ML/ml_compiler.ML"
    7.10      "ML/ml_compiler_polyml.ML"
    7.11      "ML/ml_context.ML"
     8.1 --- a/src/Pure/ROOT.ML	Wed Mar 12 22:44:55 2014 +0100
     8.2 +++ b/src/Pure/ROOT.ML	Wed Mar 12 22:57:50 2014 +0100
     8.3 @@ -233,7 +233,7 @@
     8.4  (*basic proof engine*)
     8.5  use "Isar/proof_display.ML";
     8.6  use "Isar/attrib.ML";
     8.7 -use "ML/ml_antiquote.ML";
     8.8 +use "ML/ml_antiquotation.ML";
     8.9  use "Isar/context_rules.ML";
    8.10  use "Isar/method.ML";
    8.11  use "Isar/proof.ML";
     9.1 --- a/src/Pure/simplifier.ML	Wed Mar 12 22:44:55 2014 +0100
     9.2 +++ b/src/Pure/simplifier.ML	Wed Mar 12 22:57:50 2014 +0100
     9.3 @@ -144,7 +144,7 @@
     9.4  val the_simproc = Name_Space.get o get_simprocs;
     9.5  
     9.6  val _ = Theory.setup
     9.7 -  (ML_Antiquote.value (Binding.name "simproc")
     9.8 +  (ML_Antiquotation.value (Binding.name "simproc")
     9.9      (Args.context -- Scan.lift (Parse.position Args.name)
    9.10        >> (fn (ctxt, name) =>
    9.11          "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));