--- a/src/Doc/System/Environment.thy Wed Mar 16 22:04:38 2016 +0100
+++ b/src/Doc/System/Environment.thy Wed Mar 16 22:06:05 2016 +0100
@@ -1,4 +1,4 @@
-(*:maxLineLen=78:*)
+ (*:maxLineLen=78:*)
theory Environment
imports Base
@@ -313,12 +313,8 @@
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
Run the raw Isabelle ML process in batch mode.\<close>}
-\<close>
-
-subsubsection \<open>Options\<close>
-
-text \<open>
+ \<^medskip>
Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
started. The source is either given literally or taken from a file. Multiple
\<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
@@ -366,17 +362,20 @@
-m MODE add print mode for output
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
+ -r bootstrap from raw Poly/ML
-s system build mode for session image
Build a logic session image and run the raw Isabelle ML process
in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
+ \<^medskip>
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
- checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
- abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
- Isabelle/Pure interactively.
+ checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+ Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
+ relevant for Isabelle/Pure development.
+
+ \<^medskip>
Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
(\secref{sec:tool-process}).
--- a/src/Pure/ROOT.ML Wed Mar 16 22:04:38 2016 +0100
+++ b/src/Pure/ROOT.ML Wed Mar 16 22:06:05 2016 +0100
@@ -1,4 +1,4 @@
-(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
+(*** Isabelle/Pure bootstrap ***)
(** bootstrap phase 0: Poly/ML setup **)
--- a/src/Pure/Tools/build.scala Wed Mar 16 22:04:38 2016 +0100
+++ b/src/Pure/Tools/build.scala Wed Mar 16 22:06:05 2016 +0100
@@ -258,7 +258,8 @@
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", List("--use", "ROOT.ML", "--eval", eval),
+ ML_Process(info.options,
+ raw_ml_system = true, args = List("--use", "ROOT.ML", "--eval", eval),
cwd = info.dir.file, env = env, tree = Some(tree), store = store)
}
else {
--- a/src/Pure/Tools/ml_console.scala Wed Mar 16 22:04:38 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala Wed Mar 16 22:06:05 2016 +0100
@@ -22,6 +22,7 @@
var modes: List[String] = Nil
var no_build = false
var options = Options.init()
+ var raw_ml_system = false
var system_mode = false
val getopts = Getopts("""
@@ -33,7 +34,7 @@
-m MODE add print mode for output
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is "RAW_ML_SYSTEM"
+ -r bootstrap from raw Poly/ML
-s system build mode for session image
Build a logic session image and run the raw Isabelle ML process
@@ -45,7 +46,7 @@
"m:" -> (arg => modes = arg :: modes),
"n" -> (arg => no_build = true),
"o:" -> (arg => options = options + arg),
- "r" -> (_ => logic = "RAW_ML_SYSTEM"),
+ "r" -> (_ => raw_ml_system = true),
"s" -> (_ => system_mode = true))
val more_args = getopts(args)
@@ -53,7 +54,7 @@
// build
- if (!no_build && logic != "RAW_ML_SYSTEM" &&
+ if (!no_build && !raw_ml_system &&
!Build.build(options = options, build_heap = true, no_build = true,
dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
{
@@ -70,8 +71,8 @@
// process loop
val process =
ML_Process(options, logic = logic, args = List("-i"),
- modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"),
- store = Sessions.store(system_mode))
+ modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
+ raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
val process_output = Future.thread[Unit]("process_output") {
try {
var result = new StringBuilder(100)
--- a/src/Pure/Tools/ml_process.scala Wed Mar 16 22:04:38 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Wed Mar 16 22:06:05 2016 +0100
@@ -17,6 +17,7 @@
args: List[String] = Nil,
dirs: List[Path] = Nil,
modes: List[String] = Nil,
+ raw_ml_system: Boolean = false,
secure: Boolean = false,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
@@ -28,7 +29,7 @@
{
val logic_name = Isabelle_System.default_logic(logic)
val heaps: List[String] =
- if (logic_name == "RAW_ML_SYSTEM") Nil
+ if (raw_ml_system) Nil
else {
val session_tree = tree.getOrElse(Sessions.load(options, dirs))
(session_tree.ancestors(logic_name) ::: List(logic_name)).