1.1 --- a/libisabelle-protocol/isabelle-common/protocol.ML	Thu Jan 21 17:29:33 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,119 +0,0 @@
     1.4 -signature PROTOCOL = sig
     1.5 -  type name = string
     1.6 -  type ('i, 'o) operation =
     1.7 -    {from_lib : 'i codec,
     1.8 -     to_lib : 'o codec,
     1.9 -     action : 'i -> 'o}
    1.10 -
    1.11 -  type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
    1.12 -
    1.13 -  val default_flags : flags
    1.14 -  val join_flags : flags -> flags -> flags
    1.15 -  val print_flags : flags -> string
    1.16 -
    1.17 -  val add_operation : name -> ('i, 'o) operation -> flags -> unit
    1.18 -  val get_operation : name -> int -> XML.tree -> XML.tree
    1.19 -end
    1.20 -
    1.21 -structure Protocol: PROTOCOL = struct
    1.22 -
    1.23 -type name = string
    1.24 -type ('i, 'o) operation =
    1.25 -  {from_lib : 'i codec,
    1.26 -   to_lib : 'o codec,
    1.27 -   action : 'i -> 'o}
    1.28 -
    1.29 -type flags = {sequential: bool, bracket: bool, auto: bool}
    1.30 -
    1.31 -val default_flags = {sequential = false, bracket = false, auto = false}
    1.32 -
    1.33 -fun join_flags
    1.34 -  {sequential = seq1, bracket = br1, auto = a1}
    1.35 -  {sequential = seq2, bracket = br2, auto = a2} =
    1.36 -  {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
    1.37 -
    1.38 -fun print_flags {sequential, bracket, auto} =
    1.39 -  "({sequential=" ^ Markup.print_bool sequential ^ "," ^
    1.40 -    "bracket=" ^ Markup.print_bool bracket ^ "," ^
    1.41 -    "auto=" ^ Markup.print_bool auto ^ "})"
    1.42 -
    1.43 -type raw_operation = int -> XML.tree -> XML.tree
    1.44 -
    1.45 -exception GENERIC of string
    1.46 -
    1.47 -val operations =
    1.48 -  Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
    1.49 -
    1.50 -val requests =
    1.51 -  Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
    1.52 -
    1.53 -fun sequentialize name f =
    1.54 -  let
    1.55 -    val var = Synchronized.var ("libisabelle." ^ name) ()
    1.56 -  in
    1.57 -    fn x => Synchronized.change_result var (fn _ => (f x, ()))
    1.58 -  end
    1.59 -
    1.60 -fun bracketize f id x =
    1.61 -  let
    1.62 -    val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)]
    1.63 -    val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)]
    1.64 -    val _ = Output.protocol_message start []
    1.65 -    val res = f id x
    1.66 -    val _ = Output.protocol_message stop []
    1.67 -  in res end
    1.68 -
    1.69 -fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
    1.70 -  let
    1.71 -    fun raw _ tree =
    1.72 -      case Codec.decode from_lib tree of
    1.73 -        Codec.Success i => Codec.encode to_lib (action i)
    1.74 -      | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
    1.75 -    val raw' = raw
    1.76 -      |> (if bracket then bracketize else I)
    1.77 -      |> (if sequential then sequentialize name else I)
    1.78 -  in
    1.79 -    Synchronized.change operations (Symtab.update (name, raw'))
    1.80 -  end
    1.81 -
    1.82 -fun get_operation name =
    1.83 -  case Symtab.lookup (Synchronized.value operations) name of
    1.84 -    SOME operation => operation
    1.85 -  | NONE => fn _ => raise Fail "libisabelle: unknown command"
    1.86 -
    1.87 -val _ = Isabelle_Process.protocol_command "libisabelle"
    1.88 -  (fn id :: name :: [arg] =>
    1.89 -    let
    1.90 -      val id = Markup.parse_int id
    1.91 -      val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)]
    1.92 -      val args = YXML.parse arg
    1.93 -      fun exec f =
    1.94 -        let
    1.95 -          val future = Future.fork (fn () =>
    1.96 -            let
    1.97 -              val res = Exn.interruptible_capture (f id) args
    1.98 -              val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
    1.99 -            in
   1.100 -              Output.protocol_message response [yxml]
   1.101 -            end)
   1.102 -        in
   1.103 -          Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
   1.104 -        end
   1.105 -    in
   1.106 -      exec (get_operation name)
   1.107 -    end)
   1.108 -
   1.109 -val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
   1.110 -  (fn ids =>
   1.111 -    let
   1.112 -      fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
   1.113 -      val _ =
   1.114 -        map Markup.parse_int ids
   1.115 -        |> fold_map remove
   1.116 -        |> Synchronized.change_result requests
   1.117 -        |> map (fn NONE => () | SOME f => f ())
   1.118 -    in
   1.119 -      ()
   1.120 -    end)
   1.121 -
   1.122 -end
   1.123 \ No newline at end of file