equal
deleted
inserted
replaced
188 case None => info.options |
188 case None => info.options |
189 case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n) |
189 case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n) |
190 } |
190 } |
191 |
191 |
192 private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") |
192 private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") |
193 try { isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph) } |
193 isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph) |
194 catch { case ERROR(_) => /*error should be exposed in ML*/ } |
|
195 |
194 |
196 private val future_result: Future[Process_Result] = |
195 private val future_result: Future[Process_Result] = |
197 Future.thread("build") { |
196 Future.thread("build") { |
198 val parent = info.parent.getOrElse("") |
197 val parent = info.parent.getOrElse("") |
199 val base = deps(name) |
198 val base = deps(name) |