[ide] Remove special option -ideslave

This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.

Author: ejgallego

Makefile.build

@@ -504,7 +504,7 @@ $(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coq
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
-# a connection to coqtop -ideslave
+# a connection to coqidetop
 
 FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo	\
  ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo	\

Makefile.ide

@@ -36,7 +36,7 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 
 # Note : for just building bin/coqide, we could only consider
 # config, lib, ide and ide/utils. But the coqidetop plugin (the
-# one that will be loaded by coqtop -ideslave) refers to some
+# one that will be loaded by coqidetop) refers to some
 # core modules of coq, for instance printing/*.
 
 IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils

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

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,
@@ -429,7 +428,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. *)

lib/flags.ml

@@ -57,8 +57,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let ide_slave = ref false
-
 let raw_print = ref false
 
 let we_are_parsing = ref false

lib/flags.mli

@@ -52,9 +52,6 @@ val in_toplevel : bool ref
 
 val profile : bool
 
-(* -ide_slave: printing will be more verbose, will affect stm caching *)
-val ide_slave : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 

lib/stateid.ml

@@ -11,15 +11,11 @@
 type t = int
 let initial = 1
 let dummy = 0
-let fresh, in_range =
+let fresh =
   let cur = ref initial in
-  (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
+  fun () -> incr cur; !cur
 let to_string = string_of_int
-let of_int id =
-  (* Coqide too to parse ids too, but cannot check if they are valid.
-   * Hence we check for validity only if we are an ide slave. *)
-  if !Flags.ide_slave then assert (in_range id);
-  id
+let of_int id = id
 let to_int id = id
 let newer_than id1 id2 = id1 > id2
 

stm/asyncTaskQueue.ml

@@ -123,7 +123,7 @@ module Make(T : Task) () = struct
                 ["-worker-id"; name;
                  "-async-proofs-worker-priority";
                    CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
-        | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
+        | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
         | ("-async-proofs" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"

tools/fake_ide.ml

@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
+(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *)
 
 let error s =
   prerr_endline ("fake_id: error: "^s);
@@ -284,7 +284,7 @@ let read_command inc = Parser.parse grammar inc
 
 let usage () =
   error (Printf.sprintf
-    "A fake coqide process talking to a coqtop -ideslave.\n\
+    "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
      Usage: %s (file|-) [<coqtop>]\n\
      Input syntax is the following:\n%s\n"
      (Filename.basename Sys.argv.(0))
@@ -296,7 +296,7 @@ let main =
   if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
-  let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
+  let def_args = ["--xml_format=Ppcmds"] in
   let idetop_name = System.get_toplevel_path "coqidetop" in
   let coqtop_args, input_file = match Sys.argv with
     | [| _; f |] -> Array.of_list def_args, f

toplevel/coqargs.ml

@@ -529,7 +529,6 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-filteropts" -> { oval with filter_opts = true }
-    |"-ideslave" -> Flags.ide_slave := true; oval
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
     |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval