diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 4 | ||||
| -rw-r--r-- | ide/idetop.ml | 7 |
2 files changed, 5 insertions, 6 deletions
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. *) |