src/Pure/Tools/build.scala
changeset 65506 359fc6266a00
parent 65471 05e5bffcf1d8
child 65517 1544e61e5314
equal deleted inserted replaced
65505:741fad555d82 65506:359fc6266a00
   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)