diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.ide | 2 | ||||
| -rw-r--r-- | ide/coq.ml | 4 | ||||
| -rw-r--r-- | ide/idetop.ml | 7 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | lib/stateid.ml | 10 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
11 files changed, 15 insertions, 26 deletions
diff --git a/Makefile.build b/Makefile.build index b19841a37..5f5eaf3a4 100644 --- a/Makefile.build +++ b/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 \ diff --git a/Makefile.ide b/Makefile.ide index eca0f20d4..37f698e0c 100644 --- a/Makefile.ide +++ b/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 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/idetop.ml b/ide/idetop.ml index e40af003b..64f165cde 100644 --- a/ide/idetop.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, @@ -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. *) diff --git a/lib/flags.ml b/lib/flags.ml index 56940f1cf..7e0065beb 100644 --- a/lib/flags.ml +++ b/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 diff --git a/lib/flags.mli b/lib/flags.mli index 17776d68a..02d8a3adc 100644 --- a/lib/flags.mli +++ b/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 diff --git a/lib/stateid.ml b/lib/stateid.ml index a258d5052..5485c4bf1 100644 --- a/lib/stateid.ml +++ b/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 diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 0105f821e..85a7f1495 100644 --- a/stm/asyncTaskQueue.ml +++ b/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" diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 47bd2493f..016201128 100644 --- a/tools/fake_ide.ml +++ b/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 diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5c1ffd784..89602c9b5 100644 --- a/toplevel/coqargs.ml +++ b/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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f0e41d27c..938e9718a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2243,7 +2243,7 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end |