# HG changeset patch
# User wenzelm
# Date 1597674418 -7200
# Node ID f5722290a4d088578038a278d24fdd474264daf7
# Parent  5894859c5c8478434b42885b88f3c3ea25bda900
allow user-defined server commands via isabelle_scala_service;

diff -r 5894859c5c84 -r f5722290a4d0 NEWS
--- a/NEWS	Mon Aug 17 13:16:42 2020 +0200
+++ b/NEWS	Mon Aug 17 16:26:58 2020 +0200
@@ -172,6 +172,9 @@
 "isabelle_scala_tools" and "isabelle_file_format": minor
 INCOMPATIBILITY.
 
+* Isabelle server allows user-defined commands via
+isabelle_scala_service.
+
 * Isabelle/Phabricator setup has been updated to follow ongoing
 development: libphutil has been discontinued. Minor INCOMPATIBILITY:
 existing server installations should remove libphutil from
diff -r 5894859c5c84 -r f5722290a4d0 etc/settings
--- a/etc/settings	Mon Aug 17 13:16:42 2020 +0200
+++ b/etc/settings	Mon Aug 17 16:26:58 2020 +0200
@@ -31,6 +31,7 @@
 isabelle_scala_service 'isabelle.Scala$Handler'
 isabelle_scala_service 'isabelle.Print_Operation$Handler'
 isabelle_scala_service 'isabelle.Simplifier_Trace$Handler'
+isabelle_scala_service 'isabelle.Server_Commands'
 
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
diff -r 5894859c5c84 -r f5722290a4d0 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Aug 17 13:16:42 2020 +0200
+++ b/src/Pure/Tools/server.scala	Mon Aug 17 16:26:58 2020 +0200
@@ -60,58 +60,26 @@
 
   /* input command */
 
-  object Command
+  type Command_Body = PartialFunction[(Context, Any), Any]
+
+  abstract class Command(val command_name: String)
   {
-    type T = PartialFunction[(Context, Any), Any]
+    def command_body: Command_Body
+    override def toString: String = command_name
+  }
 
-    private val table: Map[String, T] =
-      Map(
-        "help" -> { case (_, ()) => table.keySet.toList.sorted },
-        "echo" -> { case (_, t) => t },
-        "shutdown" -> { case (context, ()) => context.server.shutdown() },
-        "cancel" ->
-          { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
-        "session_build" ->
-          { case (context, Server_Commands.Session_Build(args)) =>
-              context.make_task(task =>
-                Server_Commands.Session_Build.command(args, progress = task.progress)._1)
-          },
-        "session_start" ->
-          { case (context, Server_Commands.Session_Start(args)) =>
-              context.make_task(task =>
-                {
-                  val (res, entry) =
-                    Server_Commands.Session_Start.command(
-                      args, progress = task.progress, log = context.server.log)
-                  context.server.add_session(entry)
-                  res
-                })
-          },
-        "session_stop" ->
-          { case (context, Server_Commands.Session_Stop(id)) =>
-              context.make_task(_ =>
-                {
-                  val session = context.server.remove_session(id)
-                  Server_Commands.Session_Stop.command(session)._1
-                })
-          },
-        "use_theories" ->
-          { case (context, Server_Commands.Use_Theories(args)) =>
-              context.make_task(task =>
-                {
-                  val session = context.server.the_session(args.session_id)
-                  Server_Commands.Use_Theories.command(
-                    args, session, id = task.id, progress = task.progress)._1
-                })
-          },
-        "purge_theories" ->
-          { case (context, Server_Commands.Purge_Theories(args)) =>
-              val session = context.server.the_session(args.session_id)
-              Server_Commands.Purge_Theories.command(args, session)._1
-          })
+  class Commands(commands: Command*) extends Isabelle_System.Service
+  {
+    def entries: List[Command] = commands.toList
+  }
 
-    def unapply(name: String): Option[T] = table.get(name)
-  }
+  private lazy val command_table: Map[String, Command] =
+    (Map.empty[String, Command] /: Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries))(
+      { case (cmds, cmd) =>
+          val name = cmd.command_name
+          if (cmds.isDefinedAt(name)) error("Duplicate Isabelle server command: " + quote(name))
+          else cmds + (name -> cmd)
+      })
 
 
   /* output reply */
@@ -212,6 +180,8 @@
   {
     context =>
 
+    def command_list: List[String] = command_table.keys.toList.sorted
+
     def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
     def notify(arg: Any) { connection.notify(arg) }
     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
@@ -562,12 +532,12 @@
             case Some("") => context.notify("Command 'help' provides list of commands")
             case Some(msg) =>
               val (name, argument) = Server.Argument.split(msg)
-              name match {
-                case Server.Command(cmd) =>
+              Server.command_table.get(name) match {
+                case Some(cmd) =>
                   argument match {
                     case Server.Argument(arg) =>
-                      if (cmd.isDefinedAt((context, arg))) {
-                        Exn.capture { cmd((context, arg)) } match {
+                      if (cmd.command_body.isDefinedAt((context, arg))) {
+                        Exn.capture { cmd.command_body((context, arg)) } match {
                           case Exn.Res(task: Server.Task) =>
                             connection.reply_ok(JSON.Object(task.ident))
                             task.start
@@ -587,7 +557,7 @@
                         "Malformed argument for command " + Library.single_quote(name),
                         "argument" -> argument)
                   }
-                case _ => connection.reply_error("Bad command " + Library.single_quote(name))
+                case None => connection.reply_error("Bad command " + Library.single_quote(name))
               }
           }
         }
diff -r 5894859c5c84 -r f5722290a4d0 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Mon Aug 17 13:16:42 2020 +0200
+++ b/src/Pure/Tools/server_commands.scala	Mon Aug 17 16:26:58 2020 +0200
@@ -11,17 +11,37 @@
 {
   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)
+
+    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
+  object Session_Build extends Server.Command("session_build")
   {
     sealed case class Args(
       session: String,
@@ -91,9 +111,13 @@
           results_json)
       }
     }
+
+    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
+  object Session_Start extends Server.Command("session_start")
   {
     sealed case class Args(
       build: Session_Build.Args,
@@ -126,9 +150,20 @@
 
       (res, id -> session)
     }
+
+    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
+  object Session_Stop extends Server.Command("session_stop")
   {
     def unapply(json: JSON.T): Option[UUID.T] =
       JSON.uuid(json, "session_id")
@@ -141,9 +176,18 @@
       if (result.ok) (result_json, result)
       else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)
     }
+
+    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
+  object Use_Theories extends Server.Command("use_theories")
   {
     sealed case class Args(
       session_id: UUID.T,
@@ -241,9 +285,18 @@
 
       (result_json, result)
     }
+
+    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
+  object Purge_Theories extends Server.Command("purge_theories")
   {
     sealed case class Args(
       session_id: UUID.T,
@@ -272,5 +325,22 @@
 
       (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)