clarified error result, without JSON object from "session_build";
clarified regular result;
--- 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)
}