eliminated without magic name;
authorwenzelm
Wed Mar 16 22:06:05 2016 +0100 (2016-03-16)
changeset 626436f7ac44365d7
parent 62642 c2b38181b7f1
child 62644 c36a4495ba5f
eliminated without magic name;
src/Doc/System/Environment.thy
src/Pure/ROOT.ML
src/Pure/Tools/build.scala
src/Pure/Tools/ml_console.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Doc/System/Environment.thy	Wed Mar 16 22:04:38 2016 +0100
     1.2 +++ b/src/Doc/System/Environment.thy	Wed Mar 16 22:06:05 2016 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*:maxLineLen=78:*)
     1.5 +     (*:maxLineLen=78:*)
     1.6  
     1.7  theory Environment
     1.8  imports Base
     1.9 @@ -313,12 +313,8 @@
    1.10      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.11  
    1.12    Run the raw Isabelle ML process in batch mode.\<close>}
    1.13 -\<close>
    1.14  
    1.15 -
    1.16 -subsubsection \<open>Options\<close>
    1.17 -
    1.18 -text \<open>
    1.19 +  \<^medskip>
    1.20    Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
    1.21    started. The source is either given literally or taken from a file. Multiple
    1.22    \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
    1.23 @@ -366,17 +362,20 @@
    1.24      -m MODE      add print mode for output
    1.25      -n           no build of session image on startup
    1.26      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.27 -    -r           logic session is RAW_ML_SYSTEM
    1.28 +    -r           bootstrap from raw Poly/ML
    1.29      -s           system build mode for session image
    1.30  
    1.31    Build a logic session image and run the raw Isabelle ML process
    1.32    in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
    1.33  
    1.34 +  \<^medskip>
    1.35    Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
    1.36 -  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
    1.37 -  abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
    1.38 -  Isabelle/Pure interactively.
    1.39 +  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
    1.40  
    1.41 +  Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
    1.42 +  relevant for Isabelle/Pure development.
    1.43 +
    1.44 +  \<^medskip>
    1.45    Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
    1.46    (\secref{sec:tool-process}).
    1.47  
     2.1 --- a/src/Pure/ROOT.ML	Wed Mar 16 22:04:38 2016 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Wed Mar 16 22:06:05 2016 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
     2.5 +(*** Isabelle/Pure bootstrap ***)
     2.6  
     2.7  (** bootstrap phase 0: Poly/ML setup **)
     2.8  
     3.1 --- a/src/Pure/Tools/build.scala	Wed Mar 16 22:04:38 2016 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 16 22:06:05 2016 +0100
     3.3 @@ -258,7 +258,8 @@
     3.4              val eval =
     3.5                "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
     3.6                " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
     3.7 -            ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
     3.8 +            ML_Process(info.options,
     3.9 +              raw_ml_system = true, args = List("--use", "ROOT.ML", "--eval", eval),
    3.10                cwd = info.dir.file, env = env, tree = Some(tree), store = store)
    3.11            }
    3.12            else {
     4.1 --- a/src/Pure/Tools/ml_console.scala	Wed Mar 16 22:04:38 2016 +0100
     4.2 +++ b/src/Pure/Tools/ml_console.scala	Wed Mar 16 22:06:05 2016 +0100
     4.3 @@ -22,6 +22,7 @@
     4.4        var modes: List[String] = Nil
     4.5        var no_build = false
     4.6        var options = Options.init()
     4.7 +      var raw_ml_system = false
     4.8        var system_mode = false
     4.9  
    4.10        val getopts = Getopts("""
    4.11 @@ -33,7 +34,7 @@
    4.12      -m MODE      add print mode for output
    4.13      -n           no build of session image on startup
    4.14      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    4.15 -    -r           logic session is "RAW_ML_SYSTEM"
    4.16 +    -r           bootstrap from raw Poly/ML
    4.17      -s           system build mode for session image
    4.18  
    4.19    Build a logic session image and run the raw Isabelle ML process
    4.20 @@ -45,7 +46,7 @@
    4.21          "m:" -> (arg => modes = arg :: modes),
    4.22          "n" -> (arg => no_build = true),
    4.23          "o:" -> (arg => options = options + arg),
    4.24 -        "r" -> (_ => logic = "RAW_ML_SYSTEM"),
    4.25 +        "r" -> (_ => raw_ml_system = true),
    4.26          "s" -> (_ => system_mode = true))
    4.27  
    4.28        val more_args = getopts(args)
    4.29 @@ -53,7 +54,7 @@
    4.30  
    4.31  
    4.32        // build
    4.33 -      if (!no_build && logic != "RAW_ML_SYSTEM" &&
    4.34 +      if (!no_build && !raw_ml_system &&
    4.35            !Build.build(options = options, build_heap = true, no_build = true,
    4.36              dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
    4.37        {
    4.38 @@ -70,8 +71,8 @@
    4.39        // process loop
    4.40        val process =
    4.41          ML_Process(options, logic = logic, args = List("-i"),
    4.42 -          modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"),
    4.43 -          store = Sessions.store(system_mode))
    4.44 +          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
    4.45 +          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
    4.46        val process_output = Future.thread[Unit]("process_output") {
    4.47          try {
    4.48            var result = new StringBuilder(100)
     5.1 --- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 22:04:38 2016 +0100
     5.2 +++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 22:06:05 2016 +0100
     5.3 @@ -17,6 +17,7 @@
     5.4      args: List[String] = Nil,
     5.5      dirs: List[Path] = Nil,
     5.6      modes: List[String] = Nil,
     5.7 +    raw_ml_system: Boolean = false,
     5.8      secure: Boolean = false,
     5.9      cwd: JFile = null,
    5.10      env: Map[String, String] = Isabelle_System.settings(),
    5.11 @@ -28,7 +29,7 @@
    5.12    {
    5.13      val logic_name = Isabelle_System.default_logic(logic)
    5.14      val heaps: List[String] =
    5.15 -      if (logic_name == "RAW_ML_SYSTEM") Nil
    5.16 +      if (raw_ml_system) Nil
    5.17        else {
    5.18          val session_tree = tree.getOrElse(Sessions.load(options, dirs))
    5.19          (session_tree.ancestors(logic_name) ::: List(logic_name)).