clarified bootstrapping of Pure;
authorwenzelm
Wed Aug 22 12:07:11 2012 +0200 (2012-08-22)
changeset 48879cb5cdbb645cd
parent 48878 5e850e6fa3c3
child 48880 03232f0bb5c4
clarified bootstrapping of Pure;
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/pure_syn.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 22 11:56:13 2012 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 22 12:07:11 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  val available = true;
     1.6  
     1.7 -val max_threads = ref 0;
     1.8 +val max_threads = ref 1;
     1.9  
    1.10  fun max_threads_value () =
    1.11    let val m = ! max_threads in
     2.1 --- a/src/Pure/ROOT	Wed Aug 22 11:56:13 2012 +0200
     2.2 +++ b/src/Pure/ROOT	Wed Aug 22 12:07:11 2012 +0200
     2.3 @@ -226,6 +226,7 @@
     2.4      "pattern.ML"
     2.5      "primitive_defs.ML"
     2.6      "proofterm.ML"
     2.7 +    "pure_syn.ML"
     2.8      "pure_thy.ML"
     2.9      "raw_simplifier.ML"
    2.10      "search.ML"
     3.1 --- a/src/Pure/ROOT.ML	Wed Aug 22 11:56:13 2012 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Wed Aug 22 12:07:11 2012 +0200
     3.3 @@ -303,44 +303,15 @@
     3.4  use "ProofGeneral/proof_general_emacs.ML";
     3.5  
     3.6  
     3.7 -(* ML toplevel use commands *)
     3.8 -
     3.9 -fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    3.10 -
    3.11 -fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    3.12 -fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    3.13 -
    3.14 -
    3.15  (* the Pure theory *)
    3.16  
    3.17 -val _ =
    3.18 -  Outer_Syntax.command
    3.19 -    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
    3.20 -    (Thy_Header.args >> (fn header =>
    3.21 -      Toplevel.print o
    3.22 -        Toplevel.init_theory
    3.23 -          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    3.24 +use "pure_syn.ML";
    3.25 +Thy_Info.use_thy "Pure";
    3.26 +Context.set_thread_data NONE;
    3.27 +structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    3.28  
    3.29 -val _ =
    3.30 -  Outer_Syntax.command
    3.31 -    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
    3.32 -    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
    3.33 -      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
    3.34 -        let
    3.35 -          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
    3.36 -          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
    3.37 -        in
    3.38 -          gthy
    3.39 -          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    3.40 -          |> Local_Theory.propagate_ml_env
    3.41 -          |> Context.mapping provide (Local_Theory.background_theory provide)
    3.42 -        end)));
    3.43  
    3.44 -Unsynchronized.setmp Multithreading.max_threads 1
    3.45 -  use_thy "Pure";
    3.46 -Context.set_thread_data NONE;
    3.47 -
    3.48 -structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    3.49 +use "ProofGeneral/pgip_tests.ML";
    3.50  
    3.51  
    3.52  (* ML toplevel pretty printing *)
    3.53 @@ -366,11 +337,15 @@
    3.54  if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
    3.55  
    3.56  
    3.57 -(* misc *)
    3.58 +(* ML toplevel commands *)
    3.59 +
    3.60 +fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    3.61 +
    3.62 +fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    3.63 +fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    3.64  
    3.65  val cd = File.cd o Path.explode;
    3.66  
    3.67  Proofterm.proofs := 0;
    3.68 +Multithreading.max_threads := 0;
    3.69  
    3.70 -use "ProofGeneral/pgip_tests.ML";
    3.71 -
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/pure_syn.ML	Wed Aug 22 12:07:11 2012 +0200
     4.3 @@ -0,0 +1,34 @@
     4.4 +(*  Title:      Pure/pure_syn.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Minimal outer syntax for bootstrapping Pure.
     4.8 +*)
     4.9 +
    4.10 +structure Pure_Syn: sig end =
    4.11 +struct
    4.12 +
    4.13 +val _ =
    4.14 +  Outer_Syntax.command
    4.15 +    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
    4.16 +    (Thy_Header.args >> (fn header =>
    4.17 +      Toplevel.print o
    4.18 +        Toplevel.init_theory
    4.19 +          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    4.20 +
    4.21 +val _ =
    4.22 +  Outer_Syntax.command
    4.23 +    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
    4.24 +    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
    4.25 +      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
    4.26 +        let
    4.27 +          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
    4.28 +          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
    4.29 +        in
    4.30 +          gthy
    4.31 +          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    4.32 +          |> Local_Theory.propagate_ml_env
    4.33 +          |> Context.mapping provide (Local_Theory.background_theory provide)
    4.34 +        end)));
    4.35 +
    4.36 +end;
    4.37 +