# HG changeset patch
# User wenzelm
# Date 1510513930 -3600
# Node ID 2efa25302f347699471df179dc896b109109dbf8
# Parent  9ad7bf553ee182bd141454cab8030e4deb7355c8
synchronous session start (similar to isabelle.vscode.Server);

diff -r 9ad7bf553ee1 -r 2efa25302f34 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 19:47:18 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 20:12:10 2017 +0100
@@ -9,6 +9,43 @@
 
 object Thy_Resources
 {
+  /* PIDE session */
+
+  def start_session(
+    options: Options,
+    session_name: String,
+    session_dirs: List[Path] = Nil,
+    modes: List[String] = Nil,
+    log: Logger = No_Logger): Session =
+  {
+    val session_base = Sessions.base_info(options, session_name, dirs = session_dirs).check_base
+    val resources = new Thy_Resources(session_base, log = log)
+    val session = new Session(options, resources)
+
+    val session_error = Future.promise[String]
+    var session_phase: Session.Consumer[Session.Phase] = null
+    session_phase =
+      Session.Consumer(getClass.getName) {
+        case Session.Ready =>
+          session.phase_changed -= session_phase
+          session_error.fulfill("")
+        case Session.Terminated(result) if !result.ok =>
+          session.phase_changed -= session_phase
+          session_error.fulfill("Prover startup failed: return code " + result.rc)
+        case _ =>
+      }
+    session.phase_changed += session_phase
+
+    Isabelle_Process.start(session, options,
+      logic = session_name, dirs = session_dirs, modes = modes)
+
+    session_error.join match {
+      case "" => session
+      case msg => session.stop(); error(msg)
+    }
+  }
+
+
   /* internal state */
 
   sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty)