Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ML_Env;
authorwenzelm
Mon, 01 Jun 2009 15:26:00 +0200
changeset 31327 ffa5356cc343
parent 31326 deddd77112b7
child 31328 0d3aa0aeb96f
ML_Env;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions
src/Pure/ML/ml_test.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/am_compiler.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/am_sml.ML file | annotate | diff | comparison | revisions
src/Tools/code/code_ml.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -296,11 +296,11 @@
 (* use ML text *)
 
 fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
   | propagate_env context = context;
 
 fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
+  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
 
 val _ =
   OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
--- a/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -24,7 +24,7 @@
 );
 
 fun inherit_env context =
-  ML_Context.inherit_env context #>
+  ML_Env.inherit context #>
   Extra_Env.put (Extra_Env.get context);
 
 fun register_tokens toks context =
@@ -155,7 +155,7 @@
         error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-val eval = use_text ML_Context.local_context;
+val eval = use_text ML_Env.local_context;
 
 
 (* ML test command *)
--- a/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -185,7 +185,7 @@
 
     in
 	compiled_rewriter := NONE;	
-	use_text ML_Context.local_context (1, "") false (!buffer);
+	use_text ML_Env.local_context (1, "") false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; r)
--- a/src/Tools/Compute_Oracle/am_sml.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -492,7 +492,7 @@
 
 fun writeTextFile name s = File.write (Path.explode name) s
 
-fun use_source src = use_text ML_Context.local_context (1, "") false src
+fun use_source src = use_text ML_Env.local_context (1, "") false src
     
 fun compile cache_patterns const_arity eqs = 
     let
--- a/src/Tools/code/code_ml.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -1081,7 +1081,7 @@
 fun isar_seri_sml module_name =
   Code_Target.parse_args (Scan.succeed ())
   #> (fn () => serialize_ml target_SML
-      (SOME (use_text ML_Context.local_context (1, "generated code") false))
+      (SOME (use_text ML_Env.local_context (1, "generated code") false))
       pr_sml_module pr_sml_stmt module_name);
 
 fun isar_seri_ocaml module_name =
isabelle