--- 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
--- 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"
--- 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))
}
}
}
--- 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)