--- a/NEWS Sat Nov 16 17:04:17 2013 +0100
+++ b/NEWS Sat Nov 16 17:39:11 2013 +0100
@@ -62,6 +62,15 @@
instead of explicitly stating boundedness of sets.
+*** ML ***
+
+* Toplevel function "use" refers to raw ML bootstrap environment,
+without Isar context nor antiquotations. Potential INCOMPATIBILITY.
+Note that 'ML_file' is the canonical command to load ML files into the
+formal context.
+
+
+
New in Isabelle2013-1 (November 2013)
-------------------------------------
--- a/src/Pure/ROOT.ML Sat Nov 16 17:04:17 2013 +0100
+++ b/src/Pure/ROOT.ML Sat Nov 16 17:39:11 2013 +0100
@@ -341,8 +341,6 @@
(* ML toplevel commands *)
-fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
-
fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
val use_thy = use_thys o single;
--- a/src/Pure/Thy/thy_load.ML Sat Nov 16 17:04:17 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Sat Nov 16 17:39:11 2013 +0100
@@ -18,8 +18,6 @@
val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
val loaded_files: theory -> Path.T list
val loaded_files_current: theory -> bool
- val use_ml: Path.T -> unit
- val exec_ml: Path.T -> generic_theory -> generic_theory
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
Position.T -> string -> theory list -> theory * (unit -> unit) * int
@@ -176,29 +174,6 @@
| SOME ((_, id'), _) => id = id'));
-(* provide files *)
-
-fun eval_file path text = ML_Context.eval_text true (Path.position path) text;
-
-fun use_ml src_path =
- if is_none (Context.thread_data ()) then
- let val path = check_file Path.current src_path
- in eval_file path (File.read path) end
- else
- let
- val thy = ML_Context.the_global_context ();
-
- val ((path, id), text) = load_file thy src_path;
- val _ = eval_file path text;
- val _ = Context.>> Local_Theory.propagate_ml_env;
-
- val provide = provide (src_path, id);
- val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide));
- in () end;
-
-fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
-
-
(* load_thy *)
fun begin_theory master_dir {name, imports, keywords} parents =