27 files changed, 40 insertions, 51 deletions
diff --git a/ide/utils/configwin.ml b/ide/configwin.ml
index 69e8b647a..69e8b647a 100644
--- a/ide/utils/configwin.ml
+++ b/ide/configwin.ml
diff --git a/ide/utils/configwin.mli b/ide/configwin.mli
index 7616e471d..7616e471d 100644
--- a/ide/utils/configwin.mli
+++ b/ide/configwin.mli
diff --git a/ide/utils/configwin_ihm.ml b/ide/configwin_ihm.ml
index d16efa603..d16efa603 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
diff --git a/ide/utils/configwin_ihm.mli b/ide/configwin_ihm.mli
index c867ad912..c867ad912 100644
--- a/ide/utils/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
diff --git a/ide/utils/configwin_messages.ml b/ide/configwin_messages.ml
index de1b4721d..de1b4721d 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/configwin_messages.ml
diff --git a/ide/utils/configwin_types.mli b/ide/configwin_types.ml
index 9e339d135..9e339d135 100644
--- a/ide/utils/configwin_types.mli
+++ b/ide/configwin_types.ml
diff --git a/ide/coq.ml b/ide/coq.ml
index 65456d685..63986935a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -152,7 +152,7 @@ let print_status = function
 let check_connection args =
   let lines = ref [] in
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in
+  let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
   let cmd = requote cmd in
   try
     let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
@@ -377,7 +377,7 @@ let spawn_handle args respawner feedback_processor =
     else
       "on"
   in
-  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: args) in
   let env =
     match !ideslave_coqtop_flags with
     | None -> None
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 78fbce5c8..6c3438a4b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -362,7 +362,12 @@ object(self)
     let query = Coq.query (route_id,(phrase,sid)) in
     Coq.bind (Coq.seq action query) next
 
+  method private still_valid { edit_id = id } =
+    try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true
+    with Not_found -> false
+
   method private mark_as_needed sentence =
+   if self#still_valid sentence then begin
     Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
@@ -383,6 +388,7 @@ object(self)
     in
     List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
     List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
+   end
 
   method private attach_tooltip ?loc sentence text =
     let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 96ea8c410..a7ade7130 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,15 +9,7 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Serialize
-Richprinter
-Xml_lexer
-Xml_parser
-Xml_printer
-Serialize
-Richpp
 Topfmt
-Xmlprotocol
 Ideutils
 Coq
 Coq_lex
diff --git a/ide/coqidetop.mllib b/ide/ide_common.mllib
index df988d8f1..050c282ef 100644
--- a/ide/coqidetop.mllib
+++ b/ide/ide_common.mllib
@@ -5,4 +5,3 @@ Serialize
 Richpp
 Xmlprotocol
 Document
-Ide_slave
diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli
deleted file mode 100644
index 9db9ecd12..000000000
--- a/ide/ide_slave.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* This empty file avoids a race condition that occurs when compiling a .ml file
-   that does not have a corresponding .mli file *)
diff --git a/ide/ide_slave.ml b/ide/idetop.ml
index 2e552b60b..ba69c4185 100644
--- a/ide/ide_slave.ml
+++ b/ide/idetop.ml
@@ -18,9 +18,8 @@ open Printer
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
-(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
-    function and a rewind function. This specialized loop is triggered
-    when the -ideslave option is passed to Coqtop. *)
+(** Idetop : an implementation of [Interface], i.e. mainly an interp
+    function and a rewind function. *)
 
 
 (** Signal handling: we postpone ^C during input and output phases,
@@ -273,7 +272,10 @@ let status force =
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
   Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
+  Interface.coq_object_object =
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Pp.string_of_ppcmds (pr_lconstr_env env sigma t.Search.coq_object_object)
 }
 
 let pattern_of_string ?env s =
@@ -283,7 +285,7 @@ let pattern_of_string ?env s =
     | Some e -> e
   in
   let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-  let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in
+  let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in
   pat
 
 let dirpath_of_string_list s =
@@ -352,7 +354,6 @@ let about () = {
 }
 
 let handle_exn (e, info) =
-  let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in
   let dummy = Stateid.dummy in
   let loc_of e = match Loc.get_loc e with
     | Some loc -> Some (Loc.unloc loc)
@@ -430,7 +431,7 @@ let eval_call c =
   Xmlprotocol.abstract_eval_call handler c
 
 (** Message dispatching.
-    Since coqtop -ideslave starts 1 thread per slave, and each
+    Since [coqidetop] starts 1 thread per slave, and each
     thread forwards feedback messages from the slave to the GUI on the same
     xml channel, we need mutual exclusion.  The mutex should be per-channel, but
     here we only use 1 channel. *)
@@ -458,7 +459,7 @@ let msg_format = ref (fun () ->
 
 (* The loop ignores the command line arguments as the current model delegates
    its handing to the toplevel container. *)
-let loop _args ~state =
+let loop ~opts:_ ~state =
   let open Vernac.State in
   set_doc state.doc;
   init_signal_handler ();
@@ -507,14 +508,16 @@ let rec parse = function
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let () = Coqtop.toploop_init := (fun coq_args extra_args ->
-        let args = parse extra_args in
-        Flags.quiet := true;
-        CoqworkmgrApi.(init High);
-        args)
-
-let () = Coqtop.toploop_run := loop
-
 let () = Usage.add_to_usage "coqidetop"
 "  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
+
+let islave_init ~opts extra_args =
+  let args = parse extra_args in
+  CoqworkmgrApi.(init High);
+  opts, args
+
+let () =
+  let open Coqtop in
+  let custom = { init = islave_init; run = loop; } in
+  start_coq custom
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bdb39e94a..e96b99299 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -289,16 +289,10 @@ let coqtop_path () =
     | Some s -> s
     | None ->
       match cmd_coqtop#get with
-	| Some s -> s
-	| None ->
-	  try
-            let old_prog = Sys.executable_name in
-            let pos = String.length old_prog - 6 in
-            let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
-            in
-            let new_prog = Bytes.of_string old_prog in
-            Bytes.blit_string "coqtop" 0 new_prog i 6;
-            let new_prog = Bytes.to_string new_prog in
+      | Some s -> s
+      | None ->
+        try
+          let new_prog = System.get_toplevel_path "coqidetop" in
             if Sys.file_exists new_prog then new_prog
 	    else
 	      let in_macos_bundle =
@@ -306,8 +300,8 @@ let coqtop_path () =
 		  (Filename.dirname new_prog)
 		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
 	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
-		 else "coqtop"
-	  with Not_found -> "coqtop"
+                 else "coqidetop"
+        with Not_found -> "coqidetop"
   in file
 
 (* In win32, when a command-line is to be executed via cmd.exe
diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib
new file mode 100644
index 000000000..8317a0868
--- /dev/null
+++ b/ide/protocol/ideprotocol.mllib
@@ -0,0 +1,7 @@
+Xml_lexer
+Xml_parser
+Xml_printer
+Serialize
+Richpp
+Interface
+Xmlprotocol
diff --git a/ide/interface.mli b/ide/protocol/interface.ml
index debbc8301..debbc8301 100644
--- a/ide/interface.mli
+++ b/ide/protocol/interface.ml
diff --git a/ide/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c1..19e9799c1 100644
--- a/ide/richpp.ml
+++ b/ide/protocol/richpp.ml
diff --git a/ide/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56f..31fc7b56f 100644
--- a/ide/richpp.mli
+++ b/ide/protocol/richpp.mli
diff --git a/ide/serialize.ml b/ide/protocol/serialize.ml
index 86074d44d..86074d44d 100644
--- a/ide/serialize.ml
+++ b/ide/protocol/serialize.ml
diff --git a/ide/serialize.mli b/ide/protocol/serialize.mli
index af082f25b..af082f25b 100644
--- a/ide/serialize.mli
+++ b/ide/protocol/serialize.mli
diff --git a/ide/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055f..e61cb055f 100644
--- a/ide/xml_lexer.mli
+++ b/ide/protocol/xml_lexer.mli
diff --git a/ide/xml_lexer.mll b/ide/protocol/xml_lexer.mll
index 4a52147e1..4a52147e1 100644
--- a/ide/xml_lexer.mll
+++ b/ide/protocol/xml_lexer.mll
diff --git a/ide/xml_parser.ml b/ide/protocol/xml_parser.ml
index 8db3f9e8b..8db3f9e8b 100644
--- a/ide/xml_parser.ml
+++ b/ide/protocol/xml_parser.ml
diff --git a/ide/xml_parser.mli b/ide/protocol/xml_parser.mli
index ac2eab352..ac2eab352 100644
--- a/ide/xml_parser.mli
+++ b/ide/protocol/xml_parser.mli
diff --git a/ide/xml_printer.ml b/ide/protocol/xml_printer.ml
index 488ef7bf5..488ef7bf5 100644
--- a/ide/xml_printer.ml
+++ b/ide/protocol/xml_printer.ml
diff --git a/ide/xml_printer.mli b/ide/protocol/xml_printer.mli
index 178f7c808..178f7c808 100644
--- a/ide/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210..e18219210 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
diff --git a/ide/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0a..ba6000f0a 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli