src/Pure/ROOT.ML
changeset 48879 cb5cdbb645cd
parent 48876 157dd47032e0
child 48927 ef462b5558eb
     1.1 --- a/src/Pure/ROOT.ML	Wed Aug 22 11:56:13 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Aug 22 12:07:11 2012 +0200
     1.3 @@ -303,44 +303,15 @@
     1.4  use "ProofGeneral/proof_general_emacs.ML";
     1.5  
     1.6  
     1.7 -(* ML toplevel use commands *)
     1.8 -
     1.9 -fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    1.10 -
    1.11 -fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    1.12 -fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    1.13 -
    1.14 -
    1.15  (* the Pure theory *)
    1.16  
    1.17 -val _ =
    1.18 -  Outer_Syntax.command
    1.19 -    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
    1.20 -    (Thy_Header.args >> (fn header =>
    1.21 -      Toplevel.print o
    1.22 -        Toplevel.init_theory
    1.23 -          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    1.24 +use "pure_syn.ML";
    1.25 +Thy_Info.use_thy "Pure";
    1.26 +Context.set_thread_data NONE;
    1.27 +structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    1.28  
    1.29 -val _ =
    1.30 -  Outer_Syntax.command
    1.31 -    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
    1.32 -    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
    1.33 -      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
    1.34 -        let
    1.35 -          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
    1.36 -          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
    1.37 -        in
    1.38 -          gthy
    1.39 -          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    1.40 -          |> Local_Theory.propagate_ml_env
    1.41 -          |> Context.mapping provide (Local_Theory.background_theory provide)
    1.42 -        end)));
    1.43  
    1.44 -Unsynchronized.setmp Multithreading.max_threads 1
    1.45 -  use_thy "Pure";
    1.46 -Context.set_thread_data NONE;
    1.47 -
    1.48 -structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    1.49 +use "ProofGeneral/pgip_tests.ML";
    1.50  
    1.51  
    1.52  (* ML toplevel pretty printing *)
    1.53 @@ -366,11 +337,15 @@
    1.54  if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
    1.55  
    1.56  
    1.57 -(* misc *)
    1.58 +(* ML toplevel commands *)
    1.59 +
    1.60 +fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    1.61 +
    1.62 +fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    1.63 +fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    1.64  
    1.65  val cd = File.cd o Path.explode;
    1.66  
    1.67  Proofterm.proofs := 0;
    1.68 +Multithreading.max_threads := 0;
    1.69  
    1.70 -use "ProofGeneral/pgip_tests.ML";
    1.71 -