aboutsummaryrefslogtreecommitdiff
path: root/lib/serialize.ml
diff options
context:
space:
mode:
authorEnrico Tassi2013-11-25 10:13:32 +0100
committerEnrico Tassi2013-11-27 15:12:45 +0100
commitd5451ad4fc55c38ea0a7a1687dfc80c2bb0f9d13 (patch)
tree49eabbe2d581daff058760b86708395ad997e9e4 /lib/serialize.ml
parent217793d60211c88dbeb565a3fc62994a96a062ef (diff)
First stab at retrocompatible INTERP message
Diffstat (limited to 'lib/serialize.ml')
-rw-r--r--lib/serialize.ml13
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 743247faf6..37856b5279 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -572,6 +572,8 @@ type 'a call =
| Quit of quit_sty
| About of about_sty
| Init of init_sty
+ (* retrocompatibility *)
+ | Interp of interp_sty
let str_of_call = function
| Add _ -> "Add"
@@ -589,6 +591,7 @@ let str_of_call = function
| Quit _ -> "Quit"
| About _ -> "About"
| Init _ -> "Init"
+ | Interp _ -> "Interp"
type unknown
@@ -607,6 +610,7 @@ let mkcases x : mkcases_rty call = MkCases x
let search x : search_rty call = Search x
let quit x : quit_rty call = Quit x
let init x : init_rty call = Init x
+let interp x : interp_rty call = Interp x
let abstract_eval_call handler (c : 'a call) : 'a value =
let mkGood x : 'a value = Good (Obj.magic x) in
@@ -627,6 +631,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
| Quit x -> mkGood (handler.quit x)
| About x -> mkGood (handler.about x)
| Init x -> mkGood (handler.init x)
+ | Interp x -> mkGood (handler.interp x)
with any ->
Fail (handler.handle_exn any)
@@ -648,6 +653,7 @@ let mkcases_sty_t : mkcases_sty val_t = string_t
let quit_sty_t : quit_sty val_t = unit_t
let about_sty_t : about_sty val_t = unit_t
let init_sty_t : init_sty val_t = unit_t
+let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
let add_rty_t : add_rty val_t =
pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
@@ -669,6 +675,7 @@ let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t)
let quit_rty_t : quit_rty val_t = unit_t
let about_rty_t : about_rty val_t = coq_info_t
let init_rty_t : init_rty val_t = state_id_t
+let interp_rty_t : interp_rty val_t = union_t string_t string_t
(** brain dead code, edit if protocol messages are added/removed {{{ *)
let of_answer (q : 'a call) (v : 'a value) : xml = match q with
@@ -687,6 +694,7 @@ let of_answer (q : 'a call) (v : 'a value) : xml = match q with
| Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v)
| About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v)
| Init _ -> of_value (of_value_type init_rty_t ) (Obj.magic v)
+ | Interp _ -> of_value (of_value_type interp_rty_t ) (Obj.magic v)
let to_answer (q : 'a call) (x : xml) : 'a value = match q with
| Add _ -> Obj.magic (to_value (to_value_type add_rty_t ) x)
@@ -704,6 +712,7 @@ let to_answer (q : 'a call) (x : xml) : 'a value = match q with
| Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x)
| About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x)
| Init _ -> Obj.magic (to_value (to_value_type init_rty_t ) x)
+ | Interp _ -> Obj.magic (to_value (to_value_type interp_rty_t ) x)
let of_call (q : 'a call) : xml =
let mkCall x = constructor "call" (str_of_call q) [x] in
@@ -723,6 +732,7 @@ let of_call (q : 'a call) : xml =
| Quit x -> mkCall (of_value_type quit_sty_t x)
| About x -> mkCall (of_value_type about_sty_t x)
| Init x -> mkCall (of_value_type init_sty_t x)
+ | Interp x -> mkCall (of_value_type interp_sty_t x)
let to_call : xml -> unknown call =
do_match "call" (fun s a ->
@@ -743,6 +753,7 @@ let to_call : xml -> unknown call =
| "Quit" -> Quit (mkCallArg quit_sty_t a)
| "About" -> About (mkCallArg about_sty_t a)
| "Init" -> Init (mkCallArg init_sty_t a)
+ | "Interp" -> Interp (mkCallArg interp_sty_t a)
| _ -> raise Marshal_error)
(* }}} *)
@@ -777,6 +788,7 @@ let pr_full_value call value = match call with
| Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value)
| About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value)
| Init _ -> pr_value_gen (print init_rty_t ) (Obj.magic value)
+ | Interp _ -> pr_value_gen (print interp_rty_t ) (Obj.magic value)
let pr_call call = match call with
| Add x -> str_of_call call ^ " " ^ print add_sty_t x
| Edit_at x -> str_of_call call ^ " " ^ print edit_at_sty_t x
@@ -793,6 +805,7 @@ let pr_call call = match call with
| Quit x -> str_of_call call ^ " " ^ print quit_sty_t x
| About x -> str_of_call call ^ " " ^ print about_sty_t x
| Init x -> str_of_call call ^ " " ^ print init_sty_t x
+ | Interp x -> str_of_call call ^ " " ^ print interp_sty_t x
(* }}} *)