# HG changeset patch
# User wenzelm
# Date 1521656810 -3600
# Node ID 9f82f6cc3bfca53402e734d2dcee45f601ef8b3a
# Parent  d58fa3ed236ff9bbfbee747adb00b9d9d179b41e
clarified error result, without JSON object from "session_build";
clarified regular result;

diff -r d58fa3ed236f -r 9f82f6cc3bfc src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Wed Mar 21 18:30:17 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Wed Mar 21 19:26:50 2018 +0100
@@ -124,7 +124,9 @@
     def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
       : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
     {
-      val base_info = Session_Build.command(args.build, progress = progress)._3
+      val base_info =
+        try { Session_Build.command(args.build, progress = progress)._3 }
+        catch { case exn: Server.Error => error(exn.message) }
 
       val session =
         Thy_Resources.start_session(
@@ -137,7 +139,7 @@
           log = log)
 
       val id = UUID()
-      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id.toString)
+      val res = JSON.Object("session" -> base_info.session, "session_id" -> id.toString)
 
       (res, id -> session)
     }