clarified error result, without JSON object from "session_build";
authorwenzelm
Wed, 21 Mar 2018 19:26:50 +0100
changeset 67914 9f82f6cc3bfc
parent 67913 d58fa3ed236f
child 67915 d827728b74b3
clarified error result, without JSON object from "session_build"; clarified regular result;
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)
     }