src/Pure/Tools/server_commands.scala

 
 object Server_Commands
 {
   def default_preferences: String = Options.read_prefs()
 
-  object Cancel
+  object Help extends Server.Command("help")
+  {
+    override val command_body: Server.Command_Body =
+      { case (context, ()) => context.command_list }
+  }
+
+  object Echo extends Server.Command("echo")
+  {
+    override val command_body: Server.Command_Body =
+      { case (_, t) => t }
+  }
+
+  object Cancel extends Server.Command("cancel")
   {
     sealed case class Args(task: UUID.T)
 
     def unapply(json: JSON.T): Option[Args] =
       for { task <- JSON.uuid(json, "task") }
       yield Args(task)
-  }
-
-
-  object Session_Build
+
+    override val command_body: Server.Command_Body =
+      { case (context, Cancel(args)) => context.cancel_task(args.task) }
+  }
+
+  object Shutdown extends Server.Command("shutdown")
+  {
+    override val command_body: Server.Command_Body =
+      { case (context, ()) => context.server.shutdown() }
+  }
+
+  object Session_Build extends Server.Command("session_build")
   {
     sealed case class Args(
       session: String,
       preferences: String = default_preferences,
       options: List[String] = Nil,

       else {
         throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc),
           results_json)
       }
     }
-  }
-
-  object Session_Start
+
+    override val command_body: Server.Command_Body =
+      { case (context, Session_Build(args)) =>
+        context.make_task(task => Session_Build.command(args, progress = task.progress)._1) }
+  }
+
+  object Session_Start extends Server.Command("session_start")
   {
     sealed case class Args(
       build: Session_Build.Args,
       print_mode: List[String] = Nil)
 

           "session_id" -> id.toString,
           "tmp_dir" -> File.path(session.tmp_dir).implode)
 
       (res, id -> session)
     }
-  }
-
-  object Session_Stop
+
+    override val command_body: Server.Command_Body =
+      { case (context, Session_Start(args)) =>
+          context.make_task(task =>
+          {
+            val (res, entry) =
+              Session_Start.command(args, progress = task.progress, log = context.server.log)
+            context.server.add_session(entry)
+            res
+          })
+      }
+  }
+
+  object Session_Stop extends Server.Command("session_stop")
   {
     def unapply(json: JSON.T): Option[UUID.T] =
       JSON.uuid(json, "session_id")
 
     def command(session: Headless.Session): (JSON.Object.T, Process_Result) =

       val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
 
       if (result.ok) (result_json, result)
       else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)
     }
-  }
-
-  object Use_Theories
+
+    override val command_body: Server.Command_Body =
+      { case (context, Session_Stop(id)) =>
+        context.make_task(_ =>
+        {
+          val session = context.server.remove_session(id)
+          Session_Stop.command(session)._1
+        })
+      }
+  }
+
+  object Use_Theories extends Server.Command("use_theories")
   {
     sealed case class Args(
       session_id: UUID.T,
       theories: List[String],
       master_dir: String = "",

                   }))
             }))
 
       (result_json, result)
     }
-  }
-
-  object Purge_Theories
+
+    override val command_body: Server.Command_Body =
+      { case (context, Use_Theories(args)) =>
+        context.make_task(task =>
+        {
+          val session = context.server.the_session(args.session_id)
+          Use_Theories.command(args, session, id = task.id, progress = task.progress)._1
+        })
+      }
+  }
+
+  object Purge_Theories extends Server.Command("purge_theories")
   {
     sealed case class Args(
       session_id: UUID.T,
       theories: List[String] = Nil,
       master_dir: String = "",

       val result_json =
         JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))
 
       (result_json, (purged, retained))
     }
+
+    override val command_body: Server.Command_Body =
+      { case (context, Purge_Theories(args)) =>
+        val session = context.server.the_session(args.session_id)
+        command(args, session)._1
+      }
   }
 }
+
+class Server_Commands extends Server.Commands(
+  Server_Commands.Help,
+  Server_Commands.Echo,
+  Server_Commands.Cancel,
+  Server_Commands.Shutdown,
+  Server_Commands.Session_Build,
+  Server_Commands.Session_Start,
+  Server_Commands.Session_Stop,
+  Server_Commands.Use_Theories,
+  Server_Commands.Purge_Theories)