--- a/src/Pure/System/bash.ML Fri Aug 27 21:56:42 2021 +0200
+++ b/src/Pure/System/bash.ML Sat Aug 28 12:33:43 2021 +0200
@@ -19,6 +19,12 @@
val redirect: params -> params
val timeout: Time.time -> params -> params
val description: string -> params -> params
+ val server_run: string
+ val server_kill: string
+ val server_uuid: string
+ val server_interrupt: string
+ val server_failure: string
+ val server_result: string
end;
structure Bash: BASH =
@@ -91,4 +97,15 @@
end;
+
+(* server messages *)
+
+val server_run = "run";
+val server_kill = "kill";
+
+val server_uuid = "uuid";
+val server_interrupt = "interrupt";
+val server_failure = "failure";
+val server_result = "result";
+
end;