# HG changeset patch
# User wenzelm
# Date 1265562288 -3600
# Node ID 1ec0a3ff229e4d835d19d4fcd6b2ac2bb077dd44
# Parent  a84351e7490db55e0fd4214e1617ad8b5a4c5152
simplified interface for ML antiquotations, struct_name is always "Isabelle";

diff -r a84351e7490d -r 1ec0a3ff229e src/Pure/ML/ml_antiquote.ML
--- 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";
diff -r a84351e7490d -r 1ec0a3ff229e src/Pure/ML/ml_context.ML
--- 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) =
diff -r a84351e7490d -r 1ec0a3ff229e src/Pure/ML/ml_thms.ML
--- 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;
diff -r a84351e7490d -r 1ec0a3ff229e src/Tools/Code/code_eval.ML
--- 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*)