clarified bootstrapping of Pure;

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 22 11:56:13 2012 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 22 12:07:11 2012 +0200
@@ -29,7 +29,7 @@
 
 val available = true;
 
-val max_threads = ref 0;
+val max_threads = ref 1;
 
 fun max_threads_value () =
   let val m = ! max_threads in

--- a/src/Pure/ROOT	Wed Aug 22 11:56:13 2012 +0200
+++ b/src/Pure/ROOT	Wed Aug 22 12:07:11 2012 +0200
@@ -226,6 +226,7 @@
     "pattern.ML"
     "primitive_defs.ML"
     "proofterm.ML"
+    "pure_syn.ML"
     "pure_thy.ML"
     "raw_simplifier.ML"
     "search.ML"

--- a/src/Pure/ROOT.ML	Wed Aug 22 11:56:13 2012 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 22 12:07:11 2012 +0200
@@ -303,44 +303,15 @@
 use "ProofGeneral/proof_general_emacs.ML";
 
 
-(* ML toplevel use commands *)
-
-fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
-
-fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
-fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
-
-
 (* the Pure theory *)
 
-val _ =
-  Outer_Syntax.command
-    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
-    (Thy_Header.args >> (fn header =>
-      Toplevel.print o
-        Toplevel.init_theory
-          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
+use "pure_syn.ML";
+Thy_Info.use_thy "Pure";
+Context.set_thread_data NONE;
+structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
 
-val _ =
-  Outer_Syntax.command
-    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
-    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
-      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
-        let
-          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
-          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
-        in
-          gthy
-          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
-          |> Local_Theory.propagate_ml_env
-          |> Context.mapping provide (Local_Theory.background_theory provide)
-        end)));
 
-Unsynchronized.setmp Multithreading.max_threads 1
-  use_thy "Pure";
-Context.set_thread_data NONE;
-
-structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
+use "ProofGeneral/pgip_tests.ML";
 
 
 (* ML toplevel pretty printing *)
@@ -366,11 +337,15 @@
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
 
-(* misc *)
+(* ML toplevel commands *)
+
+fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
+
+fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
+fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
 
 val cd = File.cd o Path.explode;
 
 Proofterm.proofs := 0;
+Multithreading.max_threads := 0;
 
-use "ProofGeneral/pgip_tests.ML";
-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/pure_syn.ML	Wed Aug 22 12:07:11 2012 +0200
@@ -0,0 +1,34 @@
+(*  Title:      Pure/pure_syn.ML
+    Author:     Makarius
+
+Minimal outer syntax for bootstrapping Pure.
+*)
+
+structure Pure_Syn: sig end =
+struct
+
+val _ =
+  Outer_Syntax.command
+    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
+    (Thy_Header.args >> (fn header =>
+      Toplevel.print o
+        Toplevel.init_theory
+          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
+
+val _ =
+  Outer_Syntax.command
+    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
+    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
+      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
+        let
+          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
+          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
+        in
+          gthy
+          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
+          |> Local_Theory.propagate_ml_env
+          |> Context.mapping provide (Local_Theory.background_theory provide)
+        end)));
+
+end;
+