support for "session_start";

--- a/src/Pure/Thy/sessions.scala	Thu Mar 15 16:16:19 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 15 21:26:39 2018 +0100
@@ -358,6 +358,8 @@
   /* base info */
 
   sealed case class Base_Info(
+    options: Options,
+    dirs: List[Path],
     session: String,
     sessions_structure: Structure,
     errors: List[String],
@@ -443,7 +445,7 @@
     val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
     val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
 
-    Base_Info(session1, sessions1, deps1.errors, base1, infos1)
+    Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
   }
 
 

--- a/src/Pure/Thy/thy_resources.scala	Thu Mar 15 16:16:19 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Thu Mar 15 21:26:39 2018 +0100
@@ -13,11 +13,11 @@
 
   def start_session(
     options: Options,
-    progress: Progress = No_Progress,
     session_name: String,
     session_dirs: List[Path] = Nil,
     session_base: Option[Sessions.Base] = None,
-    modes: List[String] = Nil,
+    print_mode: List[String] = Nil,
+    progress: Progress = No_Progress,
     log: Logger = No_Logger): Session =
   {
     val base =
@@ -35,13 +35,13 @@
           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)
+          session_error.fulfill("Session start failed: return code " + result.rc)
         case _ =>
       }
     session.phase_changed += session_phase
 
     Isabelle_Process.start(session, options,
-      logic = session_name, dirs = session_dirs, modes = modes)
+      logic = session_name, dirs = session_dirs, modes = print_mode)
 
     session_error.join match {
       case "" => session

--- a/src/Pure/Tools/server.scala	Thu Mar 15 16:16:19 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 15 21:26:39 2018 +0100
@@ -72,6 +72,16 @@
           { case (context, Server_Commands.Session_Build(args)) =>
               context.make_task(task =>
                 Server_Commands.Session_Build.command(task.progress, args)._1)
+          },
+        "session_start" ->
+          { case (context, Server_Commands.Session_Start(args)) =>
+              context.make_task(task =>
+                {
+                  val (res, session_id, session) =
+                    Server_Commands.Session_Start.command(task.progress, args, log = context.logger())
+                  // FIXME store session in context
+                  res
+                })
           })
 
     def unapply(name: String): Option[T] = table.get(name)

--- a/src/Pure/Tools/server_commands.scala	Thu Mar 15 16:16:19 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Thu Mar 15 21:26:39 2018 +0100
@@ -90,4 +90,39 @@
       else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
     }
   }
+
+  object Session_Start
+  {
+    sealed case class Args(
+      build: Session_Build.Args,
+      print_mode: List[String] = Nil)
+
+    def unapply(json: JSON.T): Option[Args] =
+      for {
+        build <- Session_Build.unapply(json)
+        print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _)
+      }
+      yield Args(build = build, print_mode = print_mode)
+
+    def command(progress: Progress, args: Args, log: Logger = No_Logger)
+      : (JSON.Object.T, String, Session) =
+    {
+      val base_info = Session_Build.command(progress, args.build)._3
+
+      val session =
+        Thy_Resources.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 id = Library.UUID()
+      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id)
+
+      (res, id, session)
+    }
+  }
 }