# HG changeset patch
# User wenzelm
# Date 1459935457 -7200
# Node ID b04e9fe292239c03f1161336162d36769ab1c2d9
# Parent  3c4161728aa82de6ccfc7568ef1a64e8f61983d3
clarified ML bootstrap;

diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML/ml_pervasive0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive0.ML	Wed Apr 06 11:37:37 2016 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/ML/ml_pervasive0.ML
+    Author:     Makarius
+
+Pervasive ML environment: initial setup.
+*)
+
+structure PolyML_Pretty =
+struct
+  datatype context = datatype PolyML.context;
+  datatype pretty = datatype PolyML.pretty;
+end;
+
+val seconds = Time.fromReal;
+
+val _ =
+  List.app ML_Name_Space.forget_val
+    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
+
+val ord = SML90.ord;
+val chr = SML90.chr;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+val pointer_eq = PolyML.pointerEq;
+
+val error_depth = PolyML.error_depth;
+
+open Thread;
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML/ml_pervasive1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:37:37 2016 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Pure/ML/ml_pervasive1.ML
+    Author:     Makarius
+
+Pervasive ML environment: final setup.
+*)
+
+if Options.default_bool "ML_system_bootstrap" then ()
+else
+  (List.app ML_Name_Space.forget_structure
+    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+
+structure Output: OUTPUT = Output;  (*seal system channels!*)
+
+Proofterm.proofs := 0;
+
+Context.set_thread_data NONE;
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML/ml_pervasive_final.ML
--- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 22:31:28 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/ML/ml_pervasive_final.ML
-    Author:     Makarius
-
-Pervasive ML environment: final setup.
-*)
-
-if Options.default_bool "ML_system_bootstrap" then ()
-else
-  (List.app ML_Name_Space.forget_structure
-    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
-   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
-
-structure Output: OUTPUT = Output;  (*seal system channels!*)
-
-Proofterm.proofs := 0;
-
-Context.set_thread_data NONE;
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML/ml_pervasive_initial.ML
--- a/src/Pure/ML/ml_pervasive_initial.ML	Tue Apr 05 22:31:28 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(*  Title:      Pure/ML/ml_pervasive_initial.ML
-    Author:     Makarius
-
-Pervasive ML environment: initial setup.
-*)
-
-structure PolyML_Pretty =
-struct
-  datatype context = datatype PolyML.context;
-  datatype pretty = datatype PolyML.pretty;
-end;
-
-val seconds = Time.fromReal;
-
-val _ =
-  List.app ML_Name_Space.forget_val
-    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-val pointer_eq = PolyML.pointerEq;
-
-val error_depth = PolyML.error_depth;
-
-open Thread;
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML/ml_root.scala
--- a/src/Pure/ML/ml_root.scala	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/ML/ml_root.scala	Wed Apr 06 11:37:37 2016 +0200
@@ -11,8 +11,6 @@
 {
   /* parser */
 
-  val ROOT_ML = Path.explode("ROOT.ML")
-
   val USE = "use"
   val USE_DEBUG = "use_debug"
   val USE_NO_DEBUG = "use_no_debug"
@@ -27,27 +25,23 @@
 
   private object Parser extends Parse.Parser
   {
-    val entry: Parser[(String, String)] =
-      (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG) | command(USE_THY)) ~!
-        (string ~ $$$(";")) ^^ { case a ~ (b ~ _) => (a, b) }
+    val entry: Parser[Path] =
+      command(USE_THY) ~! string ^^
+        { case _ ~ a => Resources.thy_path(Path.explode(a)) } |
+      (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG)) ~! string ^^
+        { case _ ~ a => Path.explode(a) }
 
-    def parse(in: Token.Reader): ParseResult[List[(String, String)]] =
-      parse_all(rep(entry), in)
+    val entries: Parser[List[Path]] =
+      rep(entry <~ $$$(";"))
   }
 
-  def read(dir: Path): List[(String, Path)] =
+  def read_files(root: Path): List[Path] =
   {
-    val root = dir + ROOT_ML
-
     val toks = Token.explode(syntax.keywords, File.read(root))
     val start = Token.Pos.file(root.implode)
 
-    Parser.parse(Token.reader(toks, start)) match {
-      case Parser.Success(entries, _) =>
-        for ((a, b) <- entries) yield {
-          val path = dir + Path.explode(b)
-          (a, if (a == USE_THY) Resources.thy_path(path) else path)
-        }
+    Parser.parse_all(Parser.entries, Token.reader(toks, start)) match {
+      case Parser.Success(entries, _) => entries
       case bad => error(bad.toString)
     }
   }
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML_Root.thy
--- a/src/Pure/ML_Root.thy	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/ML_Root.thy	Wed Apr 06 11:37:37 2016 +0200
@@ -7,7 +7,6 @@
 theory ML_Root
 imports Pure
 keywords "use" "use_debug" "use_no_debug" :: thy_load
-  and "use_thy" :: thy_load ("thy")
 begin
 
 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
@@ -30,11 +29,6 @@
     "read and evaluate Isabelle/ML or SML file (no debugger information)"
     (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
 
-val _ =
-  Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
-    (Parse.path -- @{keyword ";"} >> (fn _ =>
-      Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
-
 in end
 \<close>
 
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/ROOT	Wed Apr 06 11:37:37 2016 +0200
@@ -5,5 +5,3 @@
     Pure
   theories
     ML_Root
-  files
-    "ROOT.ML"
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 06 11:37:37 2016 +0200
@@ -1,26 +1,19 @@
 (*** Isabelle/Pure bootstrap ***)
 
+use "ML/ml_name_space.ML";
+
+
 (** bootstrap phase 0: Poly/ML setup **)
 
-(* initial ML name space *)
-
-use "ML/ml_name_space.ML";
-use "ML/ml_pervasive_initial.ML";
+use "ML/ml_pervasive0.ML";
 use "ML/ml_system.ML";
-
-
-(* multithreading *)
+use "System/distribution.ML";
 
 use "General/exn.ML";
 
 use "Concurrent/multithreading.ML";
 use "Concurrent/unsynchronized.ML";
 
-
-(* ML system *)
-
-use "System/distribution.ML";
-
 use "ML/ml_heap.ML";
 use "ML/ml_profiling.ML";
 use "ML/ml_print_depth0.ML";
@@ -335,8 +328,3 @@
 use_no_debug "Tools/debugger.ML";
 use "Tools/named_theorems.ML";
 use "Tools/jedit.ML";
-
-use_thy "Pure";
-
-use "ML/ml_pervasive_final.ML";
-use_thy "ML_Root";
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ROOT0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ROOT0.ML	Wed Apr 06 11:37:37 2016 +0200
@@ -0,0 +1,2 @@
+(*** Isabelle/Pure bootstrap: initial setup ***)
+
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ROOT1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ROOT1.ML	Wed Apr 06 11:37:37 2016 +0200
@@ -0,0 +1,6 @@
+(*** Isabelle/Pure bootstrap: final setup ***)
+
+use_thy "Pure";
+
+use "ML/ml_pervasive1.ML";
+use_thy "ML_Root";
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 06 11:37:37 2016 +0200
@@ -16,9 +16,17 @@
 
 object Sessions
 {
-  /* info */
+  /* Pure */
+
+  def pure_name(name: String): Boolean = name == "Pure"
+
+  val pure_roots: List[Path] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML").map(Path.explode(_))
 
-  def is_pure(name: String): Boolean = name == "Pure"
+  def pure_files(dir: Path): List[Path] =
+    (pure_roots ::: pure_roots.flatMap(root => ML_Root.read_files(dir + root))).map(dir + _)
+
+
+  /* info */
 
   sealed case class Info(
     chapter: String,
@@ -221,8 +229,8 @@
           val name = entry.name
 
           if (name == "") error("Bad session name")
-          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
-          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
+          if (pure_name(name) && entry.parent.isDefined) error("Illegal parent session")
+          if (!pure_name(name) && !entry.parent.isDefined) error("Missing parent session")
 
           val session_options = options ++ entry.options
 
diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 06 11:37:37 2016 +0200
@@ -175,8 +175,8 @@
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
               if (inlined_files)
-                thy_deps.loaded_files :::
-                  (if (Sessions.is_pure(name)) ML_Root.read(info.dir).map(_._2) else Nil)
+                (if (Sessions.pure_name(name)) Sessions.pure_files(info.dir) else Nil) :::
+                  thy_deps.loaded_files
               else Nil
 
             val all_files =
@@ -256,12 +256,13 @@
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
         val process =
-          if (Sessions.is_pure(name)) {
+          if (Sessions.pure_name(name)) {
+            val roots = Sessions.pure_roots.flatMap(root => List("--use", File.platform_path(root)))
             val eval =
               "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
               " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
             ML_Process(info.options,
-              raw_ml_system = true, args = List("--use", "ROOT.ML", "--eval", eval),
+              raw_ml_system = true, args = roots ::: List("--eval", eval),
               cwd = info.dir.file, env = env, tree = Some(tree), store = store)
           }
           else {
@@ -316,7 +317,7 @@
     {
       val result = future_result.join
 
-      if (result.ok && !Sessions.is_pure(name))
+      if (result.ok && !Sessions.pure_name(name))
         Present.finish(progress, store.browser_info, graph_file, info, name)
 
       graph_file.delete
@@ -596,7 +597,7 @@
                 val ancestor_results = selected_tree.ancestors(name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
-                val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
+                val do_output = build_heap || Sessions.pure_name(name) || queue.is_inner(name)
 
                 val (current, heap_stamp) =
                 {
@@ -673,7 +674,7 @@
       val browser_chapters =
         (for {
           (name, result) <- results0.iterator
-          if result.ok && !Sessions.is_pure(name)
+          if result.ok && !Sessions.pure_name(name)
           info = full_tree(name)
           if info.options.bool("browser_info")
         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).