--- a/src/Pure/General/secure.ML Sun Apr 06 14:30:26 2014 +0200
+++ b/src/Pure/General/secure.ML Sun Apr 06 15:19:22 2014 +0200
@@ -58,15 +58,3 @@
end;
-(*override previous toplevel bindings!*)
-val use_text = Secure.use_text;
-val use_file = Secure.use_file;
-
-fun use s =
- Position.setmp_thread_data (Position.file_only s)
- (fn () =>
- Secure.use_file ML_Parse.global_context true s
- handle ERROR msg => (writeln msg; error "ML error")) ();
-
-val toplevel_pp = Secure.toplevel_pp;
-
--- a/src/Pure/ML/ml_context.ML Sun Apr 06 14:30:26 2014 +0200
+++ b/src/Pure/ML/ml_context.ML Sun Apr 06 15:19:22 2014 +0200
@@ -188,7 +188,3 @@
end;
-fun use s =
- ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
- handle ERROR msg => (writeln msg; error "ML error");
-
--- a/src/Pure/ROOT.ML Sun Apr 06 14:30:26 2014 +0200
+++ b/src/Pure/ROOT.ML Sun Apr 06 15:19:22 2014 +0200
@@ -38,6 +38,16 @@
use "ML/ml_parse.ML";
use "General/secure.ML";
+val use_text = Secure.use_text;
+val use_file = Secure.use_file;
+
+fun use s =
+ Position.setmp_thread_data (Position.file_only s)
+ (fn () =>
+ Secure.use_file ML_Parse.global_context true s
+ handle ERROR msg => (writeln msg; error "ML error")) ();
+
+val toplevel_pp = Secure.toplevel_pp;
(** bootstrap phase 1: towards ML within Isar context *)
@@ -236,6 +246,10 @@
use "ML/ml_context.ML";
use "ML/ml_antiquotation.ML";
+fun use s =
+ ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
+ handle ERROR msg => (writeln msg; error "ML error");
+
(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)