# HG changeset patch
# User wenzelm
# Date 1458162365 -3600
# Node ID 6f7ac44365d7467be6c8705f562c56cbd5507b35
# Parent  c2b38181b7f102cb01cfc2a542c7d46925e95a16
eliminated without magic name;

diff -r c2b38181b7f1 -r 6f7ac44365d7 src/Doc/System/Environment.thy
--- 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}).
 
diff -r c2b38181b7f1 -r 6f7ac44365d7 src/Pure/ROOT.ML
--- 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 **)
 
diff -r c2b38181b7f1 -r 6f7ac44365d7 src/Pure/Tools/build.scala
--- 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 {
diff -r c2b38181b7f1 -r 6f7ac44365d7 src/Pure/Tools/ml_console.scala
--- 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)
diff -r c2b38181b7f1 -r 6f7ac44365d7 src/Pure/Tools/ml_process.scala
--- 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)).