# HG changeset patch
# User haftmann
# Date 1285945609 -7200
# Node ID 2b44308473106d7749a387285c4d8ef2b28aaea5
# Parent  10097e0a9dbd4534b2f846a1a0c24827764add3f
moved ML_Context.value to Code_Runtime

diff -r 10097e0a9dbd -r 2b4430847310 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Oct 01 16:05:25 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Oct 01 17:06:49 2010 +0200
@@ -36,9 +36,6 @@
   val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
   val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
     Context.generic -> Context.generic
-  val value: Proof.context ->
-    (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
-    string * string -> 'a
 end
 
 structure ML_Context: ML_CONTEXT =
@@ -215,17 +212,6 @@
     (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
       ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
 
-fun value ctxt (get, put, put_ml) (prelude, value) =
-  let
-    val code = (prelude
-      ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
-    val ctxt' = ctxt
-      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
-      |> Context.proof_map (exec
-          (fn () => Secure.use_text ML_Env.local_context (0, "value") false code));
-  in get ctxt' () end;
-
 end;
 
 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
diff -r 10097e0a9dbd -r 2b4430847310 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Fri Oct 01 16:05:25 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Fri Oct 01 17:06:49 2010 +0200
@@ -2,7 +2,7 @@
     Author:  Florian Haftmann, TU Muenchen
 *)
 
-header {* Loading the code generator modules *}
+header {* Loading the code generator and related modules *}
 
 theory Code_Generator
 imports Pure
@@ -21,8 +21,8 @@
   "~~/src/Tools/Code/code_ml.ML"
   "~~/src/Tools/Code/code_haskell.ML"
   "~~/src/Tools/Code/code_scala.ML"
-  "~~/src/Tools/nbe.ML"
   ("~~/src/Tools/Code/code_runtime.ML")
+  ("~~/src/Tools/nbe.ML")
 begin
 
 setup {*
@@ -32,7 +32,6 @@
   #> Code_ML.setup
   #> Code_Haskell.setup
   #> Code_Scala.setup
-  #> Nbe.setup
   #> Quickcheck.setup
 *}
 
@@ -64,6 +63,9 @@
 qed  
 
 use "~~/src/Tools/Code/code_runtime.ML"
+use "~~/src/Tools/nbe.ML"
+
+setup Nbe.setup
 
 hide_const (open) holds
 
diff -r 10097e0a9dbd -r 2b4430847310 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Oct 01 16:05:25 2010 +0200
+++ b/src/Tools/nbe.ML	Fri Oct 01 17:06:49 2010 +0200
@@ -396,7 +396,7 @@
         s
         |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
         |> pair ""
-        |> ML_Context.value ctxt univs_cookie
+        |> Code_Runtime.value ctxt univs_cookie
         |> (fn f => f deps_vals)
         |> (fn univs => cs ~~ univs)
       end;