--- 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;
--- 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
--- 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;