# HG changeset patch
# User wenzelm
# Date 1546096284 -3600
# Node ID 892b68f932f9fc7d81a7b113f222cec5dbd139ca
# Parent  e3a9680d9ed8062746b1c35a46e5d56d2248b442
clarified signature;

diff -r e3a9680d9ed8 -r 892b68f932f9 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Dec 29 14:58:51 2018 +0100
+++ b/src/Pure/PIDE/headless.scala	Sat Dec 29 16:11:24 2018 +0100
@@ -16,47 +16,6 @@
 {
   /** session **/
 
-  def start_session(
-    options: Options,
-    session_name: String,
-    session_dirs: List[Path] = Nil,
-    include_sessions: List[String] = Nil,
-    session_base: Option[Sessions.Base] = None,
-    print_mode: List[String] = Nil,
-    progress: Progress = No_Progress,
-    log: Logger = No_Logger): Session =
-  {
-    val base =
-      session_base getOrElse
-        Sessions.base_info(options, session_name, include_sessions = include_sessions,
-          progress = progress, dirs = session_dirs).check_base
-    val resources = new Resources(base, log = log)
-    val session = new Session(session_name, 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("Session start failed: return code " + result.rc)
-        case _ =>
-      }
-    session.phase_changed += session_phase
-
-    progress.echo("Starting session " + session_name + " ...")
-    Isabelle_Process.start(session, options,
-      logic = session_name, dirs = session_dirs, modes = print_mode)
-
-    session_error.join match {
-      case "" => session
-      case msg => session.stop(); error(msg)
-    }
-  }
-
   private def stable_snapshot(
     state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
   {
@@ -330,6 +289,23 @@
 
   object Resources
   {
+    def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
+      new Resources(base_info, log = log)
+
+    def make(
+      options: Options,
+      session_name: String,
+      session_dirs: List[Path] = Nil,
+      include_sessions: List[String] = Nil,
+      progress: Progress = No_Progress,
+      log: Logger = No_Logger): Resources =
+    {
+      val base_info =
+        Sessions.base_info(options, session_name, dirs = session_dirs,
+          include_sessions = include_sessions, progress = progress)
+      apply(base_info, log = log)
+    }
+
     final class Theory private[Headless](
       val node_name: Document.Node.Name,
       val node_header: Document.Node.Header,
@@ -450,11 +426,48 @@
     }
   }
 
-  class Resources(session_base: Sessions.Base, log: Logger = No_Logger)
-    extends isabelle.Resources(session_base, log = log)
+  class Resources private[Headless](
+      val session_base_info: Sessions.Base_Info,
+      log: Logger = No_Logger)
+    extends isabelle.Resources(session_base_info.check_base, log = log)
   {
     resources =>
 
+
+    /* session */
+
+    def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
+    {
+      val options = session_base_info.options
+      val session = new Session(session_base_info.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("Session start failed: return code " + result.rc)
+          case _ =>
+        }
+      session.phase_changed += session_phase
+
+      progress.echo("Starting session " + session_base_info.session + " ...")
+      Isabelle_Process.start(session, options,
+        logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode)
+
+      session_error.join match {
+        case "" => session
+        case msg => session.stop(); error(msg)
+      }
+    }
+
+
+    /* theories */
+
     private val state = Synchronized(Resources.State())
 
     def load_theories(
diff -r e3a9680d9ed8 -r 892b68f932f9 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Dec 29 14:58:51 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Dec 29 16:11:24 2018 +0100
@@ -150,11 +150,13 @@
 
     /* run session */
 
-    val session =
-      Headless.start_session(dump_options, logic, progress = progress, log = log,
+    val resources =
+      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
         session_dirs = dirs ::: select_dirs,
         include_sessions = deps.sessions_structure.imports_topological_order)
 
+    val session = resources.start_session(progress = progress)
+
     try {
       val use_theories_result =
         session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
diff -r e3a9680d9ed8 -r 892b68f932f9 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Dec 29 14:58:51 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Sat Dec 29 16:11:24 2018 +0100
@@ -113,15 +113,9 @@
         try { Session_Build.command(args.build, progress = progress)._3 }
         catch { case exn: Server.Error => error(exn.message) }
 
-      val session =
-        Headless.start_session(
-          base_info.options,
-          base_info.session,
-          session_dirs = base_info.dirs,
-          session_base = Some(base_info.check_base),
-          print_mode = args.print_mode,
-          progress = progress,
-          log = log)
+      val resources = Headless.Resources(base_info, log = log)
+
+      val session = resources.start_session(print_mode = args.print_mode, progress = progress)
 
       val id = UUID.random()