|
1 signature PROTOCOL = sig |
|
2 type name = string |
|
3 type ('i, 'o) operation = |
|
4 {from_lib : 'i codec, |
|
5 to_lib : 'o codec, |
|
6 action : 'i -> 'o} |
|
7 |
|
8 type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)} |
|
9 |
|
10 val default_flags : flags |
|
11 val join_flags : flags -> flags -> flags |
|
12 val print_flags : flags -> string |
|
13 |
|
14 val add_operation : name -> ('i, 'o) operation -> flags -> unit |
|
15 val get_operation : name -> int -> XML.tree -> XML.tree |
|
16 end |
|
17 |
|
18 structure Protocol: PROTOCOL = struct |
|
19 |
|
20 type name = string |
|
21 type ('i, 'o) operation = |
|
22 {from_lib : 'i codec, |
|
23 to_lib : 'o codec, |
|
24 action : 'i -> 'o} |
|
25 |
|
26 type flags = {sequential: bool, bracket: bool, auto: bool} |
|
27 |
|
28 val default_flags = {sequential = false, bracket = false, auto = false} |
|
29 |
|
30 fun join_flags |
|
31 {sequential = seq1, bracket = br1, auto = a1} |
|
32 {sequential = seq2, bracket = br2, auto = a2} = |
|
33 {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2} |
|
34 |
|
35 fun print_flags {sequential, bracket, auto} = |
|
36 "({sequential=" ^ Markup.print_bool sequential ^ "," ^ |
|
37 "bracket=" ^ Markup.print_bool bracket ^ "," ^ |
|
38 "auto=" ^ Markup.print_bool auto ^ "})" |
|
39 |
|
40 type raw_operation = int -> XML.tree -> XML.tree |
|
41 |
|
42 exception GENERIC of string |
|
43 |
|
44 val operations = |
|
45 Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table) |
|
46 |
|
47 val requests = |
|
48 Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table) |
|
49 |
|
50 fun sequentialize name f = |
|
51 let |
|
52 val var = Synchronized.var ("libisabelle." ^ name) () |
|
53 in |
|
54 fn x => Synchronized.change_result var (fn _ => (f x, ())) |
|
55 end |
|
56 |
|
57 fun bracketize f id x = |
|
58 let |
|
59 val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)] |
|
60 val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)] |
|
61 val _ = Output.protocol_message start [] |
|
62 val res = f id x |
|
63 val _ = Output.protocol_message stop [] |
|
64 in res end |
|
65 |
|
66 fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} = |
|
67 let |
|
68 fun raw _ tree = |
|
69 case Codec.decode from_lib tree of |
|
70 Codec.Success i => Codec.encode to_lib (action i) |
|
71 | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg) |
|
72 val raw' = raw |
|
73 |> (if bracket then bracketize else I) |
|
74 |> (if sequential then sequentialize name else I) |
|
75 in |
|
76 Synchronized.change operations (Symtab.update (name, raw')) |
|
77 end |
|
78 |
|
79 fun get_operation name = |
|
80 case Symtab.lookup (Synchronized.value operations) name of |
|
81 SOME operation => operation |
|
82 | NONE => fn _ => raise Fail "libisabelle: unknown command" |
|
83 |
|
84 val _ = Isabelle_Process.protocol_command "libisabelle" |
|
85 (fn id :: name :: [arg] => |
|
86 let |
|
87 val id = Markup.parse_int id |
|
88 val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)] |
|
89 val args = YXML.parse arg |
|
90 fun exec f = |
|
91 let |
|
92 val future = Future.fork (fn () => |
|
93 let |
|
94 val res = Exn.interruptible_capture (f id) args |
|
95 val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res) |
|
96 in |
|
97 Output.protocol_message response [yxml] |
|
98 end) |
|
99 in |
|
100 Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future)) |
|
101 end |
|
102 in |
|
103 exec (get_operation name) |
|
104 end) |
|
105 |
|
106 val _ = Isabelle_Process.protocol_command "libisabelle_cancel" |
|
107 (fn ids => |
|
108 let |
|
109 fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab) |
|
110 val _ = |
|
111 map Markup.parse_int ids |
|
112 |> fold_map remove |
|
113 |> Synchronized.change_result requests |
|
114 |> map (fn NONE => () | SOME f => f ()) |
|
115 in |
|
116 () |
|
117 end) |
|
118 |
|
119 end |