--- a/src/Pure/ML/ml_antiquote.ML Sat Feb 06 23:26:17 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Sun Feb 07 18:04:48 2010 +0100
@@ -38,17 +38,17 @@
fun macro name scan = ML_Context.add_antiq name
(fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
- (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
+ (Context.Proof ctxt, fn background => (K ("", ""), background)))));
fun inline name scan = ML_Context.add_antiq name
- (fn _ => scan >> (fn s => fn {background, ...} => (K ("", s), background)));
+ (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
fun declaration kind name scan = ML_Context.add_antiq name
- (fn _ => scan >> (fn s => fn {struct_name, background} =>
+ (fn _ => scan >> (fn s => fn background =>
let
val (a, background') = variant name background;
val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
- val body = struct_name ^ "." ^ a;
+ val body = "Isabelle." ^ a;
in (K (env, body), background') end));
val value = declaration "val";
--- a/src/Pure/ML/ml_context.ML Sat Feb 06 23:26:17 2010 +0100
+++ b/src/Pure/ML/ml_context.ML Sun Feb 07 18:04:48 2010 +0100
@@ -22,9 +22,7 @@
val stored_thms: thm list Unsynchronized.ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
- type antiq =
- {struct_name: string, background: Proof.context} ->
- (Proof.context -> string * string) * Proof.context
+ type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
val trace: bool Unsynchronized.ref
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -84,9 +82,7 @@
(* antiquotation commands *)
-type antiq =
- {struct_name: string, background: Proof.context} ->
- (Proof.context -> string * string) * Proof.context;
+type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
local
@@ -123,8 +119,7 @@
P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
-val struct_name = "Isabelle";
-val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
+val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
val end_env = ML_Lex.tokenize "end;";
val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
@@ -151,7 +146,7 @@
let
val context = Stack.top scope;
val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
- val (decl, background') = f {background = background, struct_name = struct_name};
+ val (decl, background') = f background;
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
in (decl', (Stack.map_top (K context') scope, background')) end
| expand (Antiquote.Open _) (scope, background) =
--- a/src/Pure/ML/ml_thms.ML Sat Feb 06 23:26:17 2010 +0100
+++ b/src/Pure/ML/ml_thms.ML Sun Feb 07 18:04:48 2010 +0100
@@ -34,12 +34,12 @@
(* fact references *)
fun thm_antiq kind scan = ML_Context.add_antiq kind
- (fn _ => scan >> (fn ths => fn {struct_name, background} =>
+ (fn _ => scan >> (fn ths => fn background =>
let
val i = serial ();
val (a, background') = background
|> ML_Antiquote.variant kind ||> put_thms (i, ths);
- val ml = (thm_bind kind a i, struct_name ^ "." ^ a);
+ val ml = (thm_bind kind a i, "Isabelle." ^ a);
in (K ml, background') end));
val _ = thm_antiq "thm" (Attrib.thm >> single);
@@ -56,7 +56,7 @@
(fn _ => Args.context -- Args.mode "open" --
Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) --
(by |-- Method.parse -- Scan.option Method.parse)) >>
- (fn ((ctxt, is_open), (raw_propss, methods)) => fn {struct_name, background} =>
+ (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
let
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
val i = serial ();
@@ -69,8 +69,7 @@
val (a, background') = background
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
val ml =
- (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i,
- struct_name ^ "." ^ a);
+ (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
in (K ml, background') end));
end;
--- a/src/Tools/Code/code_eval.ML Sat Feb 06 23:26:17 2010 +0100
+++ b/src/Tools/Code/code_eval.ML Sun Feb 07 18:04:48 2010 +0100
@@ -107,25 +107,25 @@
val _ = map2 check_base constrs constrs'';
in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
-fun print_code struct_name is_first print_it ctxt =
+fun print_code is_first print_it ctxt =
let
val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
val ml_code = if is_first then ml_code
else "";
- val all_struct_name = Long_Name.append struct_name struct_code_name;
+ val all_struct_name = "Isabelle." ^ struct_code_name;
in (ml_code, print_it all_struct_name tycos_map consts_map) end;
in
-fun ml_code_antiq raw_const {struct_name, background} =
+fun ml_code_antiq raw_const background =
let
val const = Code.check_const (ProofContext.theory_of background) raw_const;
val is_first = is_first_occ background;
val background' = register_const const background;
- in (print_code struct_name is_first (print_const const), background') end;
+ in (print_code is_first (print_const const), background') end;
-fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
+fun ml_code_datatype_antiq (raw_tyco, raw_constrs) background =
let
val thy = ProofContext.theory_of background;
val tyco = Sign.intern_type thy raw_tyco;
@@ -135,7 +135,7 @@
else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
val is_first = is_first_occ background;
val background' = register_datatype tyco constrs background;
- in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
+ in (print_code is_first (print_datatype tyco constrs), background') end;
end; (*local*)