src/Pure/Tools/build.scala
changeset 65313 347ed6219dab
parent 65312 34d56ca5b548
child 65314 944758d6462e
     1.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 20:35:58 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 20:51:42 2017 +0100
     1.3 @@ -130,18 +130,52 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* PIDE protocol handler */
     1.8 +
     1.9 +  class Handler(progress: Progress, session: Session, session_name: String)
    1.10 +    extends Session.Protocol_Handler
    1.11 +  {
    1.12 +    val result_error: Promise[String] = Future.promise
    1.13 +
    1.14 +    override def exit() { result_error.cancel }
    1.15 +
    1.16 +    private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
    1.17 +    {
    1.18 +      val error_message =
    1.19 +        try { Pretty.string_of(YXML.parse_body(Symbol.decode(msg.text))) }
    1.20 +        catch { case ERROR(msg) => msg }
    1.21 +      result_error.fulfill(error_message)
    1.22 +      session.send_stop()
    1.23 +      true
    1.24 +    }
    1.25 +
    1.26 +    private def loading_theory(msg: Prover.Protocol_Output): Boolean =
    1.27 +      msg.properties match {
    1.28 +        case Markup.Loading_Theory(name) =>
    1.29 +          progress.theory(session_name, name)
    1.30 +          true
    1.31 +        case _ => false
    1.32 +      }
    1.33 +
    1.34 +    val functions =
    1.35 +      List(
    1.36 +        Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
    1.37 +        Markup.LOADING_THEORY -> loading_theory _)
    1.38 +  }
    1.39 +
    1.40 +
    1.41    /* job: running prover process */
    1.42  
    1.43    private class Job(progress: Progress,
    1.44      name: String,
    1.45      val info: Sessions.Info,
    1.46      tree: Sessions.Tree,
    1.47 +    deps: Sessions.Deps,
    1.48      store: Sessions.Store,
    1.49      do_output: Boolean,
    1.50      verbose: Boolean,
    1.51      pide: Boolean,
    1.52      val numa_node: Option[Int],
    1.53 -    session_graph: Graph_Display.Graph,
    1.54      command_timings: List[Properties.T])
    1.55    {
    1.56      val output = store.output_dir + Path.basic(name)
    1.57 @@ -155,7 +189,7 @@
    1.58        }
    1.59  
    1.60      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
    1.61 -    try { isabelle.graphview.Graph_File.write(options, graph_file, session_graph) }
    1.62 +    try { isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph) }
    1.63      catch { case ERROR(_) => /*error should be exposed in ML*/ }
    1.64  
    1.65      private val future_result: Future[Process_Result] =
    1.66 @@ -185,8 +219,29 @@
    1.67            "ML_Heap.share_common_data (); ML_Heap.save_child " +
    1.68              ML_Syntax.print_string0(File.platform_path(output))
    1.69  
    1.70 -        if (pide) {
    1.71 -          error("FIXME")
    1.72 +        if (pide && !Sessions.pure_name(name)) {
    1.73 +          val resources = new Resources(deps(parent))
    1.74 +          val session = new Session(options, resources)
    1.75 +          val handler = new Handler(progress, session, name)
    1.76 +          session.add_protocol_handler(handler)
    1.77 +
    1.78 +          val session_result = Future.promise[Int]
    1.79 +
    1.80 +          Isabelle_Process.start(session, options, logic = parent,
    1.81 +            cwd = info.dir.file, env = env, tree = Some(tree), store = store,
    1.82 +            phase_changed =
    1.83 +            {
    1.84 +              case Session.Ready => session.protocol_command("build_session", args_yxml)
    1.85 +              case Session.Terminated(rc) => session_result.fulfill(rc)
    1.86 +              case _ =>
    1.87 +            })
    1.88 +
    1.89 +          val rc = session_result.join
    1.90 +
    1.91 +          handler.result_error.join match {
    1.92 +            case "" => Process_Result(rc)
    1.93 +            case msg => Process_Result(rc max 1, out_lines = split_lines(Output.error_text(msg)))
    1.94 +          }
    1.95          }
    1.96          else {
    1.97            val args_file = Isabelle_System.tmp_file("build")
    1.98 @@ -496,8 +551,8 @@
    1.99                    val numa_node = numa_nodes.next(used_node(_))
   1.100                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.101                    val job =
   1.102 -                    new Job(progress, name, info, selected_tree, store, do_output, verbose,
   1.103 -                      pide, numa_node, deps(name).session_graph, queue.command_timings(name))
   1.104 +                    new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
   1.105 +                      pide, numa_node, queue.command_timings(name))
   1.106                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   1.107                  }
   1.108                  else {
   1.109 @@ -679,60 +734,4 @@
   1.110  
   1.111      sys.exit(results.rc)
   1.112    })
   1.113 -
   1.114 -
   1.115 -  /* PIDE protocol */
   1.116 -
   1.117 -  def build_theories(
   1.118 -    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
   1.119 -      session.get_protocol_handler(classOf[Handler].getName) match {
   1.120 -        case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
   1.121 -        case _ => error("Cannot invoke build_theories: bad protocol handler")
   1.122 -      }
   1.123 -
   1.124 -  class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
   1.125 -  {
   1.126 -    private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
   1.127 -
   1.128 -    override def exit(): Unit =
   1.129 -      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
   1.130 -
   1.131 -    def build_theories(
   1.132 -      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
   1.133 -    {
   1.134 -      val promise = Future.promise[XML.Body]
   1.135 -      val id = Document_ID.make().toString
   1.136 -      pending.change(promises => promises + (id -> promise))
   1.137 -      session.build_theories(id, master_dir, theories)
   1.138 -      promise
   1.139 -    }
   1.140 -
   1.141 -    private def loading_theory(msg: Prover.Protocol_Output): Boolean =
   1.142 -      msg.properties match {
   1.143 -        case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
   1.144 -        case _ => false
   1.145 -      }
   1.146 -
   1.147 -    private def build_theories_result(msg: Prover.Protocol_Output): Boolean =
   1.148 -      msg.properties match {
   1.149 -        case Markup.Build_Theories_Result(id) =>
   1.150 -          pending.change_result(promises =>
   1.151 -            promises.get(id) match {
   1.152 -              case Some(promise) =>
   1.153 -                val error_message =
   1.154 -                  try { YXML.parse_body(Symbol.decode(msg.text)) }
   1.155 -                  catch { case exn: Throwable => List(XML.Text(Exn.message(exn))) }
   1.156 -                promise.fulfill(error_message)
   1.157 -                (true, promises - id)
   1.158 -              case None =>
   1.159 -                (false, promises)
   1.160 -            })
   1.161 -        case _ => false
   1.162 -      }
   1.163 -
   1.164 -    val functions =
   1.165 -      List(
   1.166 -        Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
   1.167 -        Markup.LOADING_THEORY -> loading_theory _)
   1.168 -  }
   1.169  }