toplevel function "use" refers to raw ML bootstrap environment;
authorwenzelm
Sat Nov 16 17:39:11 2013 +0100 (2013-11-16)
changeset 54449f3cfe882f9af
parent 54448 7110476960f7
child 54450 7815563f50dc
toplevel function "use" refers to raw ML bootstrap environment;
NEWS
src/Pure/ROOT.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/NEWS	Sat Nov 16 17:04:17 2013 +0100
     1.2 +++ b/NEWS	Sat Nov 16 17:39:11 2013 +0100
     1.3 @@ -62,6 +62,15 @@
     1.4  instead of explicitly stating boundedness of sets.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Toplevel function "use" refers to raw ML bootstrap environment,
    1.10 +without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
    1.11 +Note that 'ML_file' is the canonical command to load ML files into the
    1.12 +formal context.
    1.13 +
    1.14 +
    1.15 +
    1.16  New in Isabelle2013-1 (November 2013)
    1.17  -------------------------------------
    1.18  
     2.1 --- a/src/Pure/ROOT.ML	Sat Nov 16 17:04:17 2013 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Sat Nov 16 17:39:11 2013 +0100
     2.3 @@ -341,8 +341,6 @@
     2.4  
     2.5  (* ML toplevel commands *)
     2.6  
     2.7 -fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
     2.8 -
     2.9  fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
    2.10  val use_thy = use_thys o single;
    2.11  
     3.1 --- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:04:17 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:39:11 2013 +0100
     3.3 @@ -18,8 +18,6 @@
     3.4    val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
     3.5    val loaded_files: theory -> Path.T list
     3.6    val loaded_files_current: theory -> bool
     3.7 -  val use_ml: Path.T -> unit
     3.8 -  val exec_ml: Path.T -> generic_theory -> generic_theory
     3.9    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    3.10    val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
    3.11      Position.T -> string -> theory list -> theory * (unit -> unit) * int
    3.12 @@ -176,29 +174,6 @@
    3.13        | SOME ((_, id'), _) => id = id'));
    3.14  
    3.15  
    3.16 -(* provide files *)
    3.17 -
    3.18 -fun eval_file path text = ML_Context.eval_text true (Path.position path) text;
    3.19 -
    3.20 -fun use_ml src_path =
    3.21 -  if is_none (Context.thread_data ()) then
    3.22 -    let val path = check_file Path.current src_path
    3.23 -    in eval_file path (File.read path) end
    3.24 -  else
    3.25 -    let
    3.26 -      val thy = ML_Context.the_global_context ();
    3.27 -
    3.28 -      val ((path, id), text) = load_file thy src_path;
    3.29 -      val _ = eval_file path text;
    3.30 -      val _ = Context.>> Local_Theory.propagate_ml_env;
    3.31 -
    3.32 -      val provide = provide (src_path, id);
    3.33 -      val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide));
    3.34 -    in () end;
    3.35 -
    3.36 -fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
    3.37 -
    3.38 -
    3.39  (* load_thy *)
    3.40  
    3.41  fun begin_theory master_dir {name, imports, keywords} parents =