src/Pure/ROOT.ML
changeset 56303 4cc3f4db3447
parent 56288 bf1bdf335ea0
child 56434 7acc933bd7cc
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -69,6 +69,7 @@
     1.4  
     1.5  use "PIDE/xml.ML";
     1.6  use "PIDE/yxml.ML";
     1.7 +use "PIDE/document_id.ML";
     1.8  
     1.9  use "General/change_table.ML";
    1.10  use "General/graph.ML";
    1.11 @@ -193,16 +194,18 @@
    1.12  
    1.13  (* Isar -- Intelligible Semi-Automated Reasoning *)
    1.14  
    1.15 -(*ML support*)
    1.16 +(*ML support and global execution*)
    1.17  use "ML/ml_syntax.ML";
    1.18  use "ML/ml_env.ML";
    1.19 +use "ML/ml_options.ML";
    1.20 +use "ML/exn_output.ML";
    1.21 +if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
    1.22 +use "ML/ml_options.ML";
    1.23  use "Isar/runtime.ML";
    1.24 +use "PIDE/execution.ML";
    1.25  use "ML/ml_compiler.ML";
    1.26  if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
    1.27  
    1.28 -(*global execution*)
    1.29 -use "PIDE/document_id.ML";
    1.30 -use "PIDE/execution.ML";
    1.31  use "skip_proof.ML";
    1.32  use "goal.ML";
    1.33  
    1.34 @@ -346,7 +349,7 @@
    1.35  (* the Pure theory *)
    1.36  
    1.37  use "pure_syn.ML";
    1.38 -Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
    1.39 +Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
    1.40  Context.set_thread_data NONE;
    1.41  structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    1.42  
    1.43 @@ -355,7 +358,8 @@
    1.44  
    1.45  (* ML toplevel commands *)
    1.46  
    1.47 -fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
    1.48 +fun use_thys args =
    1.49 +  Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
    1.50  val use_thy = use_thys o single;
    1.51  
    1.52  val cd = File.cd o Path.explode;