First stab at retrocompatible INTERP message

3 files changed, 23 insertions, 0 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 31577e6296..24f2b65249 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -233,6 +233,12 @@ type about_rty = coq_info
 type handle_exn_sty = exn
 type handle_exn_rty = state_id * location * string
 
+(* Retrocompatibility stuff *)
+type interp_sty = (raw * verbose) * string
+(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
+type interp_rty = (string,string) Util.union
+
+
 type handler = {
   add         : add_sty         -> add_rty;
   edit_at     : edit_at_sty     -> edit_at_rty;
@@ -250,5 +256,7 @@ type handler = {
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
   init        : init_sty        -> init_rty;
   quit        : quit_sty        -> quit_rty;
+  (* Retrocompatibility stuff *)
+  interp      : interp_sty      -> interp_rty;
 }
 
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
 
 (* }}} *)
 
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 2b1718bf76..e749462087 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -29,6 +29,8 @@ val get_options : get_options_sty -> get_options_rty call
 val set_options : set_options_sty -> set_options_rty call
 val quit        : quit_sty        -> quit_rty call
 val init        : init_sty        -> init_rty call
+(* retrocompatibility *)
+val interp      : interp_sty      -> interp_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value