more realistic PIDE build session;
authorwenzelm
Sat Mar 18 20:51:42 2017 +0100 (2017-03-18)
changeset 65313347ed6219dab
parent 65312 34d56ca5b548
child 65314 944758d6462e
more realistic PIDE build session;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Sat Mar 18 20:35:58 2017 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,64 +0,0 @@
     1.4 -/*  Title:      Pure/PIDE/batch_session.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -PIDE session in batch mode.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -import isabelle._
    1.14 -
    1.15 -
    1.16 -object Batch_Session
    1.17 -{
    1.18 -  def batch_session(
    1.19 -    options: Options,
    1.20 -    verbose: Boolean = false,
    1.21 -    dirs: List[Path] = Nil,
    1.22 -    session: String): Batch_Session =
    1.23 -  {
    1.24 -    val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session))
    1.25 -    val session_info = session_tree(session)
    1.26 -    val parent_session =
    1.27 -      session_info.parent getOrElse error("No parent session for " + quote(session))
    1.28 -
    1.29 -    if (!Build.build(options, new Console_Progress(verbose = verbose),
    1.30 -        verbose = verbose, build_heap = true,
    1.31 -        dirs = dirs, sessions = List(parent_session)).ok)
    1.32 -      throw new RuntimeException
    1.33 -
    1.34 -    val deps = Sessions.dependencies(verbose = verbose, tree = session_tree)
    1.35 -    val resources = new Resources(deps(parent_session))
    1.36 -
    1.37 -    val progress = new Console_Progress(verbose = verbose)
    1.38 -
    1.39 -    val prover_session = new Session(options, resources)
    1.40 -    val batch_session = new Batch_Session(prover_session)
    1.41 -
    1.42 -    val handler = new Build.Handler(progress, session)
    1.43 -
    1.44 -    Isabelle_Process.start(prover_session, options, logic = parent_session,
    1.45 -      phase_changed =
    1.46 -      {
    1.47 -        case Session.Ready =>
    1.48 -          prover_session.add_protocol_handler(handler)
    1.49 -          val master_dir = session_info.dir
    1.50 -          val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    1.51 -          batch_session.build_theories_result =
    1.52 -            Some(Build.build_theories(prover_session, master_dir, theories))
    1.53 -        case Session.Terminated(rc) =>
    1.54 -          batch_session.session_result.fulfill(rc)
    1.55 -        case _ =>
    1.56 -      })
    1.57 -
    1.58 -    batch_session
    1.59 -  }
    1.60 -}
    1.61 -
    1.62 -class Batch_Session private(val session: Session)
    1.63 -{
    1.64 -  val session_result = Future.promise[Int]
    1.65 -  @volatile var build_theories_result: Option[Promise[XML.Body]] = None
    1.66 -}
    1.67 -
     2.1 --- a/src/Pure/PIDE/markup.ML	Sat Mar 18 20:35:58 2017 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Sat Mar 18 20:51:42 2017 +0100
     2.3 @@ -194,7 +194,7 @@
     2.4    val command_timing: Properties.entry
     2.5    val loading_theory: string -> Properties.T
     2.6    val dest_loading_theory: Properties.T -> string option
     2.7 -  val build_theories_result: string -> Properties.T
     2.8 +  val build_session_finished: Properties.T
     2.9    val print_operationsN: string
    2.10    val print_operations: Properties.T
    2.11    val debugger_state: string -> Properties.T
    2.12 @@ -618,7 +618,7 @@
    2.13  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
    2.14    | dest_loading_theory _ = NONE;
    2.15  
    2.16 -fun build_theories_result id = [("function", "build_theories_result"), ("id", id)];
    2.17 +val build_session_finished = [("function", "build_session_finished")];
    2.18  
    2.19  val print_operationsN = "print_operations";
    2.20  val print_operations = [(functionN, print_operationsN)];
     3.1 --- a/src/Pure/PIDE/markup.scala	Sat Mar 18 20:35:58 2017 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Sat Mar 18 20:51:42 2017 +0100
     3.3 @@ -541,15 +541,8 @@
     3.4        }
     3.5    }
     3.6  
     3.7 -  val BUILD_THEORIES_RESULT = "build_theories_result"
     3.8 -  object Build_Theories_Result
     3.9 -  {
    3.10 -    def unapply(props: Properties.T): Option[String] =
    3.11 -      props match {
    3.12 -        case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id)
    3.13 -        case _ => None
    3.14 -      }
    3.15 -  }
    3.16 +  val BUILD_SESSION_FINISHED = "build_session_finished"
    3.17 +  val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
    3.18  
    3.19    val PRINT_OPERATIONS = "print_operations"
    3.20  
     4.1 --- a/src/Pure/PIDE/protocol.scala	Sat Mar 18 20:35:58 2017 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Mar 18 20:51:42 2017 +0100
     4.3 @@ -404,18 +404,4 @@
     4.4  
     4.5    def dialog_result(serial: Long, result: String): Unit =
     4.6      protocol_command("Document.dialog_result", Value.Long(serial), result)
     4.7 -
     4.8 -
     4.9 -  /* build_theories */
    4.10 -
    4.11 -  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
    4.12 -  {
    4.13 -    val symbol_codes_yxml =
    4.14 -    { import XML.Encode._
    4.15 -      YXML.string_of_body(list(pair(string, int))(Symbol.codes)) }
    4.16 -    val theories_yxml =
    4.17 -    { import XML.Encode._
    4.18 -      YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) }
    4.19 -    protocol_command("build_theories", id, master_dir.implode, theories_yxml)
    4.20 -  }
    4.21  }
     5.1 --- a/src/Pure/PIDE/session.scala	Sat Mar 18 20:35:58 2017 +0100
     5.2 +++ b/src/Pure/PIDE/session.scala	Sat Mar 18 20:51:42 2017 +0100
     5.3 @@ -514,9 +514,6 @@
     5.4              prover.get.dialog_result(serial, result)
     5.5              handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
     5.6  
     5.7 -          case Session.Build_Theories(id, master_dir, theories) if prover.defined =>
     5.8 -            prover.get.build_theories(id, master_dir, theories)
     5.9 -
    5.10            case Protocol_Command(name, args) if prover.defined =>
    5.11              prover.get.protocol_command(name, args:_*)
    5.12  
    5.13 @@ -600,7 +597,4 @@
    5.14  
    5.15    def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
    5.16    { manager.send(Session.Dialog_Result(id, serial, result)) }
    5.17 -
    5.18 -  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
    5.19 -  { manager.send(Session.Build_Theories(id, master_dir, theories)) }
    5.20  }
     6.1 --- a/src/Pure/Tools/build.ML	Sat Mar 18 20:35:58 2017 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Sat Mar 18 20:51:42 2017 +0100
     6.3 @@ -211,36 +211,12 @@
     6.4  (*PIDE version*)
     6.5  val _ =
     6.6    Isabelle_Process.protocol_command "build_session"
     6.7 -    (fn [id, yxml] =>
     6.8 +    (fn [args_yxml] =>
     6.9        let
    6.10 -        val args = decode_args yxml;
    6.11 +        val args = decode_args args_yxml;
    6.12          val result = (build_session args; "") handle exn =>
    6.13            (Runtime.exn_message exn handle _ (*sic!*) =>
    6.14              "Exception raised, but failed to print details!");
    6.15 -    in Output.protocol_message (Markup.build_theories_result id) [result] end | _ => raise Match);
    6.16 -
    6.17 -val _ =
    6.18 -  Isabelle_Process.protocol_command "build_theories"
    6.19 -    (fn [id, symbol_codes_yxml, master_dir, theories_yxml] =>
    6.20 -      let
    6.21 -        val symbols =
    6.22 -          YXML.parse_body symbol_codes_yxml
    6.23 -          |> let open XML.Decode in list (pair string int) end
    6.24 -          |> HTML.make_symbols;
    6.25 -        val theories =
    6.26 -          YXML.parse_body theories_yxml |>
    6.27 -            let open XML.Decode
    6.28 -            in list (pair Options.decode (list (string #> rpair Position.none))) end;
    6.29 -        val res1 =
    6.30 -          Exn.capture
    6.31 -            (fn () =>
    6.32 -              theories
    6.33 -              |> List.app (build_theories symbols (K Time.zeroTime) (Path.explode master_dir))) ();
    6.34 -        val res2 = Exn.capture Session.shutdown ();
    6.35 -        val result =
    6.36 -          (Par_Exn.release_all [res1, res2]; "") handle exn =>
    6.37 -            (Runtime.exn_message exn handle _ (*sic!*) =>
    6.38 -              "Exception raised, but failed to print details!");
    6.39 -    in Output.protocol_message (Markup.build_theories_result id) [result] end | _ => raise Match);
    6.40 +    in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
    6.41  
    6.42  end;
     7.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 20:35:58 2017 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 20:51:42 2017 +0100
     7.3 @@ -130,18 +130,52 @@
     7.4    }
     7.5  
     7.6  
     7.7 +  /* PIDE protocol handler */
     7.8 +
     7.9 +  class Handler(progress: Progress, session: Session, session_name: String)
    7.10 +    extends Session.Protocol_Handler
    7.11 +  {
    7.12 +    val result_error: Promise[String] = Future.promise
    7.13 +
    7.14 +    override def exit() { result_error.cancel }
    7.15 +
    7.16 +    private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
    7.17 +    {
    7.18 +      val error_message =
    7.19 +        try { Pretty.string_of(YXML.parse_body(Symbol.decode(msg.text))) }
    7.20 +        catch { case ERROR(msg) => msg }
    7.21 +      result_error.fulfill(error_message)
    7.22 +      session.send_stop()
    7.23 +      true
    7.24 +    }
    7.25 +
    7.26 +    private def loading_theory(msg: Prover.Protocol_Output): Boolean =
    7.27 +      msg.properties match {
    7.28 +        case Markup.Loading_Theory(name) =>
    7.29 +          progress.theory(session_name, name)
    7.30 +          true
    7.31 +        case _ => false
    7.32 +      }
    7.33 +
    7.34 +    val functions =
    7.35 +      List(
    7.36 +        Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
    7.37 +        Markup.LOADING_THEORY -> loading_theory _)
    7.38 +  }
    7.39 +
    7.40 +
    7.41    /* job: running prover process */
    7.42  
    7.43    private class Job(progress: Progress,
    7.44      name: String,
    7.45      val info: Sessions.Info,
    7.46      tree: Sessions.Tree,
    7.47 +    deps: Sessions.Deps,
    7.48      store: Sessions.Store,
    7.49      do_output: Boolean,
    7.50      verbose: Boolean,
    7.51      pide: Boolean,
    7.52      val numa_node: Option[Int],
    7.53 -    session_graph: Graph_Display.Graph,
    7.54      command_timings: List[Properties.T])
    7.55    {
    7.56      val output = store.output_dir + Path.basic(name)
    7.57 @@ -155,7 +189,7 @@
    7.58        }
    7.59  
    7.60      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
    7.61 -    try { isabelle.graphview.Graph_File.write(options, graph_file, session_graph) }
    7.62 +    try { isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph) }
    7.63      catch { case ERROR(_) => /*error should be exposed in ML*/ }
    7.64  
    7.65      private val future_result: Future[Process_Result] =
    7.66 @@ -185,8 +219,29 @@
    7.67            "ML_Heap.share_common_data (); ML_Heap.save_child " +
    7.68              ML_Syntax.print_string0(File.platform_path(output))
    7.69  
    7.70 -        if (pide) {
    7.71 -          error("FIXME")
    7.72 +        if (pide && !Sessions.pure_name(name)) {
    7.73 +          val resources = new Resources(deps(parent))
    7.74 +          val session = new Session(options, resources)
    7.75 +          val handler = new Handler(progress, session, name)
    7.76 +          session.add_protocol_handler(handler)
    7.77 +
    7.78 +          val session_result = Future.promise[Int]
    7.79 +
    7.80 +          Isabelle_Process.start(session, options, logic = parent,
    7.81 +            cwd = info.dir.file, env = env, tree = Some(tree), store = store,
    7.82 +            phase_changed =
    7.83 +            {
    7.84 +              case Session.Ready => session.protocol_command("build_session", args_yxml)
    7.85 +              case Session.Terminated(rc) => session_result.fulfill(rc)
    7.86 +              case _ =>
    7.87 +            })
    7.88 +
    7.89 +          val rc = session_result.join
    7.90 +
    7.91 +          handler.result_error.join match {
    7.92 +            case "" => Process_Result(rc)
    7.93 +            case msg => Process_Result(rc max 1, out_lines = split_lines(Output.error_text(msg)))
    7.94 +          }
    7.95          }
    7.96          else {
    7.97            val args_file = Isabelle_System.tmp_file("build")
    7.98 @@ -496,8 +551,8 @@
    7.99                    val numa_node = numa_nodes.next(used_node(_))
   7.100                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   7.101                    val job =
   7.102 -                    new Job(progress, name, info, selected_tree, store, do_output, verbose,
   7.103 -                      pide, numa_node, deps(name).session_graph, queue.command_timings(name))
   7.104 +                    new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
   7.105 +                      pide, numa_node, queue.command_timings(name))
   7.106                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   7.107                  }
   7.108                  else {
   7.109 @@ -679,60 +734,4 @@
   7.110  
   7.111      sys.exit(results.rc)
   7.112    })
   7.113 -
   7.114 -
   7.115 -  /* PIDE protocol */
   7.116 -
   7.117 -  def build_theories(
   7.118 -    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
   7.119 -      session.get_protocol_handler(classOf[Handler].getName) match {
   7.120 -        case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
   7.121 -        case _ => error("Cannot invoke build_theories: bad protocol handler")
   7.122 -      }
   7.123 -
   7.124 -  class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
   7.125 -  {
   7.126 -    private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
   7.127 -
   7.128 -    override def exit(): Unit =
   7.129 -      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
   7.130 -
   7.131 -    def build_theories(
   7.132 -      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
   7.133 -    {
   7.134 -      val promise = Future.promise[XML.Body]
   7.135 -      val id = Document_ID.make().toString
   7.136 -      pending.change(promises => promises + (id -> promise))
   7.137 -      session.build_theories(id, master_dir, theories)
   7.138 -      promise
   7.139 -    }
   7.140 -
   7.141 -    private def loading_theory(msg: Prover.Protocol_Output): Boolean =
   7.142 -      msg.properties match {
   7.143 -        case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
   7.144 -        case _ => false
   7.145 -      }
   7.146 -
   7.147 -    private def build_theories_result(msg: Prover.Protocol_Output): Boolean =
   7.148 -      msg.properties match {
   7.149 -        case Markup.Build_Theories_Result(id) =>
   7.150 -          pending.change_result(promises =>
   7.151 -            promises.get(id) match {
   7.152 -              case Some(promise) =>
   7.153 -                val error_message =
   7.154 -                  try { YXML.parse_body(Symbol.decode(msg.text)) }
   7.155 -                  catch { case exn: Throwable => List(XML.Text(Exn.message(exn))) }
   7.156 -                promise.fulfill(error_message)
   7.157 -                (true, promises - id)
   7.158 -              case None =>
   7.159 -                (false, promises)
   7.160 -            })
   7.161 -        case _ => false
   7.162 -      }
   7.163 -
   7.164 -    val functions =
   7.165 -      List(
   7.166 -        Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
   7.167 -        Markup.LOADING_THEORY -> loading_theory _)
   7.168 -  }
   7.169  }
     8.1 --- a/src/Pure/build-jars	Sat Mar 18 20:35:58 2017 +0100
     8.2 +++ b/src/Pure/build-jars	Sat Mar 18 20:51:42 2017 +0100
     8.3 @@ -84,7 +84,6 @@
     8.4    Isar/token.scala
     8.5    ML/ml_lex.scala
     8.6    ML/ml_syntax.scala
     8.7 -  PIDE/batch_session.scala
     8.8    PIDE/command.scala
     8.9    PIDE/command_span.scala
    8.10    PIDE/document.scala