1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/libisabelle-protocol/libisabelle/protocol/protocol.ML	Tue Sep 04 14:50:30 2018 +0200
     1.3 @@ -0,0 +1,119 @@
     1.4 +signature LIBISABELLE_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 Libisabelle_Protocol: LIBISABELLE_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=" ^ print_bool sequential ^ "," ^
    1.40 +    "bracket=" ^ print_bool bracket ^ "," ^
    1.41 +    "auto=" ^ 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", print_int id)]
    1.63 +    val stop = [(Markup.functionN, "libisabelle_stop"), ("id", 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 _ => error "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 = parse_int id
    1.91 +      val response = [(Markup.functionN, "libisabelle_response"), ("id", 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 (fn () => 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 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