# HG changeset patch
# User wenzelm
# Date 1343843600 -7200
# Node ID 22d65e375c01e3d5c59c1dbcff531783fac4c7d0
# Parent  547b075669ae700e7ddf9314d4d9b8012af8a343
more standard bootstrapping of Pure.thy;

diff -r 547b075669ae -r 22d65e375c01 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 01 19:53:20 2012 +0200
@@ -31,7 +31,6 @@
   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> Token.T list
   val parse: Position.T -> string -> Toplevel.transition list
-  val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
@@ -242,20 +241,6 @@
   |> Source.exhaust;
 
 
-(* process file *)
-
-fun process_file path thy =
-  let
-    val trs = parse (Path.position path) (File.read path);
-    val init = Toplevel.init_theory (K thy) Toplevel.empty;
-    val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
-  in
-    (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
-      (true, Context.Theory thy') => thy'
-    | _ => error "Bad result state: global theory expected")
-  end;
-
-
 (* interactive source of toplevel transformers *)
 
 type isar =
diff -r 547b075669ae -r 22d65e375c01 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/Pure.thy	Wed Aug 01 19:53:20 2012 +0200
@@ -1,3 +1,5 @@
+theory Pure
+begin
 
 section {* Further content for the Pure theory *}
 
@@ -82,3 +84,5 @@
   qed
 qed
 
+end
+
diff -r 547b075669ae -r 22d65e375c01 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML	Wed Aug 01 19:53:20 2012 +0200
@@ -97,7 +97,7 @@
 
 val args =
   theory_name --
-  (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) --
+  Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
   Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --
   Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
   Parse.$$$ beginN >>
diff -r 547b075669ae -r 22d65e375c01 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Aug 01 19:53:20 2012 +0200
@@ -62,7 +62,7 @@
 
     val args =
       theory_name ~
-      (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
+      (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       keyword(BEGIN) ^^
diff -r 547b075669ae -r 22d65e375c01 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 01 19:53:20 2012 +0200
@@ -236,7 +236,9 @@
     val {uses, keywords, ...} = Thy_Header.read pos text;
     val header = Thy_Header.make name imports keywords uses;
 
-    val (theory, present) = Thy_Load.load_thy update_time dir header pos text parents;
+    val (theory, present) =
+      Thy_Load.load_thy update_time dir header pos text
+        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in (theory, present, commit) end;
 
diff -r 547b075669ae -r 22d65e375c01 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/context.ML	Wed Aug 01 19:53:20 2012 +0200
@@ -410,7 +410,7 @@
 
       val Theory ({ids, ...}, data, _, _) =
         (case parents of
-          [] => error "No parent theories"
+          [] => error "Missing theory imports"
         | [thy] => extend_thy thy
         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
 
diff -r 547b075669ae -r 22d65e375c01 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/pure_setup.ML	Wed Aug 01 19:53:20 2012 +0200
@@ -4,16 +4,21 @@
 Pure theory and ML toplevel setup.
 *)
 
+(* 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 *)
 
-Context.>> (Context.map_theory
- (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
-  Theory.end_theory));
+Unsynchronized.setmp Multithreading.max_threads 1
+  use_thy "Pure";
+Context.set_thread_data NONE;
 
-structure Pure = struct val thy = ML_Context.the_global_context () end;
-
-Context.set_thread_data NONE;
-Thy_Info.register_thy Pure.thy;
+structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
 
 
 (* ML toplevel pretty printing *)
@@ -39,14 +44,6 @@
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
 
-(* 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);
-
-
 (* misc *)
 
 val cd = File.cd o Path.explode;
diff -r 547b075669ae -r 22d65e375c01 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/theory.ML	Wed Aug 01 19:53:20 2012 +0200
@@ -138,16 +138,19 @@
 fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
 
 fun begin_theory name imports =
-  let
-    val thy = Context.begin_thy Context.pretty_global name imports;
-    val wrappers = begin_wrappers thy;
-  in
-    thy
-    |> Sign.local_path
-    |> Sign.map_naming (Name_Space.set_theory_name name)
-    |> apply_wrappers wrappers
-    |> tap (Syntax.force_syntax o Sign.syn_of)
-  end;
+  if name = Context.PureN then
+    (case imports of [thy] => thy | _ => error "Bad bootstrapping of theory Pure")
+  else
+    let
+      val thy = Context.begin_thy Context.pretty_global name imports;
+      val wrappers = begin_wrappers thy;
+    in
+      thy
+      |> Sign.local_path
+      |> Sign.map_naming (Name_Space.set_theory_name name)
+      |> apply_wrappers wrappers
+      |> tap (Syntax.force_syntax o Sign.syn_of)
+    end;
 
 fun end_theory thy =
   thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;