# 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 \structure PolyML = struct structure IntInf = PolyML.IntInf end\); + +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 \structure PolyML = struct structure IntInf = PolyML.IntInf end\); - -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 \Context.theory_map ML_Env.init_bootstrap\ @@ -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 \ 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).