diff -r 109e995e5e3b -r 907ce624bd20 libisabelle-protocol/common/protocol.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/libisabelle-protocol/common/protocol.ML	Fri Jan 22 15:53:13 2016 +0100
@@ -0,0 +1,119 @@
+signature PROTOCOL = sig
+  type name = string
+  type ('i, 'o) operation =
+    {from_lib : 'i codec,
+     to_lib : 'o codec,
+     action : 'i -> 'o}
+
+  type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
+
+  val default_flags : flags
+  val join_flags : flags -> flags -> flags
+  val print_flags : flags -> string
+
+  val add_operation : name -> ('i, 'o) operation -> flags -> unit
+  val get_operation : name -> int -> XML.tree -> XML.tree
+end
+
+structure Protocol: PROTOCOL = struct
+
+type name = string
+type ('i, 'o) operation =
+  {from_lib : 'i codec,
+   to_lib : 'o codec,
+   action : 'i -> 'o}
+
+type flags = {sequential: bool, bracket: bool, auto: bool}
+
+val default_flags = {sequential = false, bracket = false, auto = false}
+
+fun join_flags
+  {sequential = seq1, bracket = br1, auto = a1}
+  {sequential = seq2, bracket = br2, auto = a2} =
+  {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
+
+fun print_flags {sequential, bracket, auto} =
+  "({sequential=" ^ Markup.print_bool sequential ^ "," ^
+    "bracket=" ^ Markup.print_bool bracket ^ "," ^
+    "auto=" ^ Markup.print_bool auto ^ "})"
+
+type raw_operation = int -> XML.tree -> XML.tree
+
+exception GENERIC of string
+
+val operations =
+  Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
+
+val requests =
+  Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
+
+fun sequentialize name f =
+  let
+    val var = Synchronized.var ("libisabelle." ^ name) ()
+  in
+    fn x => Synchronized.change_result var (fn _ => (f x, ()))
+  end
+
+fun bracketize f id x =
+  let
+    val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)]
+    val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)]
+    val _ = Output.protocol_message start []
+    val res = f id x
+    val _ = Output.protocol_message stop []
+  in res end
+
+fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
+  let
+    fun raw _ tree =
+      case Codec.decode from_lib tree of
+        Codec.Success i => Codec.encode to_lib (action i)
+      | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
+    val raw' = raw
+      |> (if bracket then bracketize else I)
+      |> (if sequential then sequentialize name else I)
+  in
+    Synchronized.change operations (Symtab.update (name, raw'))
+  end
+
+fun get_operation name =
+  case Symtab.lookup (Synchronized.value operations) name of
+    SOME operation => operation
+  | NONE => fn _ => raise Fail "libisabelle: unknown command"
+
+val _ = Isabelle_Process.protocol_command "libisabelle"
+  (fn id :: name :: [arg] =>
+    let
+      val id = Markup.parse_int id
+      val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)]
+      val args = YXML.parse arg
+      fun exec f =
+        let
+          val future = Future.fork (fn () =>
+            let
+              val res = Exn.interruptible_capture (f id) args
+              val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
+            in
+              Output.protocol_message response [yxml]
+            end)
+        in
+          Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
+        end
+    in
+      exec (get_operation name)
+    end)
+
+val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
+  (fn ids =>
+    let
+      fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
+      val _ =
+        map Markup.parse_int ids
+        |> fold_map remove
+        |> Synchronized.change_result requests
+        |> map (fn NONE => () | SOME f => f ())
+    in
+      ()
+    end)
+
+end
\ No newline at end of file