# HG changeset patch
# User wenzelm
# Date 1384619951 -3600
# Node ID f3cfe882f9afe5044e6dae8010a7f09a0701f303
# Parent  7110476960f732fd8a30e5850604665dcf88a8c0
toplevel function "use" refers to raw ML bootstrap environment;

diff -r 7110476960f7 -r f3cfe882f9af NEWS
--- 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)
 -------------------------------------
 
diff -r 7110476960f7 -r f3cfe882f9af src/Pure/ROOT.ML
--- 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;
 
diff -r 7110476960f7 -r f3cfe882f9af src/Pure/Thy/thy_load.ML
--- 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 =