# HG changeset patch
# User wenzelm
# Date 1585938472 -7200
# Node ID ff2c26b8ffb1c13fe56cabf08cf18fc76b959e92
# Parent  da49285a0adfab339c6fc7aa3a0fa0bf146a27ca
clarified build_options vs. job options;

diff -r da49285a0adf -r ff2c26b8ffb1 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 03 18:26:04 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 03 20:27:52 2020 +0200
@@ -162,13 +162,12 @@
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
-    private def build_options(options: Options): Options = options + "pide_reports=false"
-    private val job_options = build_options(NUMA.policy_options(info.options, numa_node))
+    val options = NUMA.policy_options(info.options, numa_node)
 
     private val sessions_structure = deps.sessions_structure
 
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
-    graphview.Graph_File.write(job_options, graph_file, deps(session_name).session_graph_display)
+    graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer =
@@ -178,8 +177,6 @@
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
         val base = deps(parent)
-        val encode_theory_options: XML.Encode.T[Options] =
-          (options => Options.encode(build_options(options)))
         val args_yxml =
           YXML.string_of_body(
             {
@@ -187,7 +184,7 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                pair(list(pair(encode_theory_options, list(pair(string, properties)))),
+                pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(string), pair(list(pair(string, string)),
@@ -205,7 +202,7 @@
         val env =
           Isabelle_System.settings() +
             ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
-            ("ISABELLE_ML_DEBUGGER" -> job_options.bool("ML_debugger").toString)
+            ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
         val is_pure = Sessions.is_pure(session_name)
 
@@ -219,9 +216,9 @@
           }
           else Nil
 
-        if (job_options.bool("pide_build")) {
+        if (options.bool("pide_build")) {
           val resources = new Resources(sessions_structure, deps(parent))
-          val session = new Session(job_options, resources)
+          val session = new Session(options, resources)
 
           val build_session_errors: Promise[List[String]] = Future.promise
           val stdout = new StringBuilder(1000)
@@ -318,7 +315,7 @@
           val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
           val process =
-            Isabelle_Process(session, job_options, sessions_structure, store,
+            Isabelle_Process(session, options, sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env)
@@ -356,7 +353,7 @@
           val eval_main = Command_Line.ML_tool(eval_build :: eval_store)
 
           val process =
-            ML_Process(job_options, deps.sessions_structure, store,
+            ML_Process(options, deps.sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
@@ -378,7 +375,7 @@
                 case _ =>
               },
             progress_limit =
-              job_options.int("process_output_limit") match {
+              options.int("process_output_limit") match {
                 case 0 => None
                 case m => Some(m * 1000000L)
               },
@@ -479,7 +476,8 @@
     sessions: List[String] = Nil,
     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   {
-    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
+    val build_options =
+      options + "pide_reports=false" + "completion_limit=0" + "ML_statistics"
 
     val store = Sessions.store(build_options)