clarified error result, without JSON object from "session_build";
authorwenzelm
Wed Mar 21 19:26:50 2018 +0100 (14 months ago)
changeset 679149f82f6cc3bfc
parent 67913 d58fa3ed236f
child 67915 d827728b74b3
clarified error result, without JSON object from "session_build";
clarified regular result;
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Tools/server_commands.scala	Wed Mar 21 18:30:17 2018 +0100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Wed Mar 21 19:26:50 2018 +0100
     1.3 @@ -124,7 +124,9 @@
     1.4      def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
     1.5        : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
     1.6      {
     1.7 -      val base_info = Session_Build.command(args.build, progress = progress)._3
     1.8 +      val base_info =
     1.9 +        try { Session_Build.command(args.build, progress = progress)._3 }
    1.10 +        catch { case exn: Server.Error => error(exn.message) }
    1.11  
    1.12        val session =
    1.13          Thy_Resources.start_session(
    1.14 @@ -137,7 +139,7 @@
    1.15            log = log)
    1.16  
    1.17        val id = UUID()
    1.18 -      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id.toString)
    1.19 +      val res = JSON.Object("session" -> base_info.session, "session_id" -> id.toString)
    1.20  
    1.21        (res, id -> session)
    1.22      }