--- /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;
--- /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;
--- 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;
--- 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;
--- 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)
}
}
--- 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>
--- 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"
--- 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";
--- /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 ***)
+
--- /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";
--- 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
--- 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).