diff options
| -rw-r--r-- | lib/interface.mli | 2 | ||||
| -rw-r--r-- | lib/serialize.ml | 2 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 24f2b6524..a01ec20ae 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -236,7 +236,7 @@ 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 interp_rty = state_id * (string,string) Util.union type handler = { diff --git a/lib/serialize.ml b/lib/serialize.ml index 2b46df60b..b1768d76d 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -651,7 +651,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 +let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) let ($) x = erase x let calls = [| diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 7a548e046..be384e174 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -323,7 +323,7 @@ let interp ((_raw, verbose), s) = | Some ast -> ast) () in Stm.interp verbose (vernac_parse s); - CSig.Inl (read_stdout ()) + Stm.get_current_state (), CSig.Inl (read_stdout ()) (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer |