src/Pure/Tools/build.scala
changeset 65312 34d56ca5b548
parent 65308 8f58102afa22
child 65313 347ed6219dab
     1.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 20:30:05 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 20:35:58 2017 +0100
     1.3 @@ -148,8 +148,14 @@
     1.4      def output_path: Option[Path] = if (do_output) Some(output) else None
     1.5      output.file.delete
     1.6  
     1.7 +    val options =
     1.8 +      numa_node match {
     1.9 +        case None => info.options
    1.10 +        case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
    1.11 +      }
    1.12 +
    1.13      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
    1.14 -    try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
    1.15 +    try { isabelle.graphview.Graph_File.write(options, graph_file, session_graph) }
    1.16      catch { case ERROR(_) => /*error should be exposed in ML*/ }
    1.17  
    1.18      private val future_result: Future[Process_Result] =
    1.19 @@ -173,7 +179,7 @@
    1.20  
    1.21          val env =
    1.22            Isabelle_System.settings() +
    1.23 -            ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
    1.24 +            ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
    1.25  
    1.26          def save_heap: String =
    1.27            "ML_Heap.share_common_data (); ML_Heap.save_child " +
    1.28 @@ -191,21 +197,16 @@
    1.29              "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
    1.30              (if (do_output) "; " + save_heap else "") + "));"
    1.31  
    1.32 -          val process_options =
    1.33 -            numa_node match {
    1.34 -              case None => info.options
    1.35 -              case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
    1.36 -            }
    1.37            val process =
    1.38              if (Sessions.pure_name(name)) {
    1.39 -              ML_Process(process_options, raw_ml_system = true, cwd = info.dir.file,
    1.40 +              ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
    1.41                  args =
    1.42                    (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    1.43                    List("--eval", eval),
    1.44                  env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    1.45              }
    1.46              else {
    1.47 -              ML_Process(process_options, parent, List("--eval", eval), cwd = info.dir.file,
    1.48 +              ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
    1.49                  env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    1.50              }
    1.51  
    1.52 @@ -216,7 +217,7 @@
    1.53                  case None =>
    1.54                },
    1.55              progress_limit =
    1.56 -              info.options.int("process_output_limit") match {
    1.57 +              options.int("process_output_limit") match {
    1.58                  case 0 => None
    1.59                  case m => Some(m * 1000000L)
    1.60                },