--- a/src/Pure/ML/ml_antiquotation.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Mon Dec 08 22:42:12 2014 +0100
@@ -6,7 +6,6 @@
signature ML_ANTIQUOTATION =
sig
- val variant: string -> Proof.context -> string * Proof.context
val declaration: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
theory -> theory
@@ -17,24 +16,6 @@
structure ML_Antiquotation: ML_ANTIQUOTATION =
struct
-(* unique names *)
-
-val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
-
-structure Names = Proof_Data
-(
- type T = Name.context;
- fun init _ = init_context;
-);
-
-fun variant a ctxt =
- let
- val names = Names.get ctxt;
- val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
- val ctxt' = Names.put names' ctxt;
- in (b, ctxt') end;
-
-
(* define antiquotations *)
fun declaration name scan body =
@@ -47,25 +28,15 @@
declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
fun value name scan =
- declaration name scan (fn _ => fn s => fn ctxt =>
- let
- val (a, ctxt') = variant (Binding.name_of name) ctxt;
- val env = "val " ^ a ^ " = " ^ s ^ ";\n";
- val body = "Isabelle." ^ a;
- in (K (env, body), ctxt') end);
+ declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
(* basic antiquotations *)
val _ = Theory.setup
(declaration (Binding.make ("here", @{here})) (Scan.succeed ())
- (fn src => fn () => fn ctxt =>
- let
- val (a, ctxt') = variant "position" ctxt;
- val (_, pos) = Token.name_of_src src;
- val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
- val body = "Isabelle." ^ a;
- in (K (env, body), ctxt') end) #>
+ (fn src => fn () =>
+ ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
value (Binding.make ("binding", @{here}))
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));