diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 4 | ||||
| -rw-r--r-- | ide/coq.mli | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 5 | ||||
| -rw-r--r-- | ide/minilib.ml | 2 | ||||
| -rw-r--r-- | ide/minilib.mli | 2 |
6 files changed, 12 insertions, 6 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 42ab86dd62..34b4875af0 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -9,6 +9,8 @@ open Ideutils open Preferences +let ideslave_coqtop_flags = ref None + (** * Version and date *) let get_version_date () = @@ -375,7 +377,7 @@ let spawn_handle args respawner feedback_processor = in let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in let env = - match !Flags.ideslave_coqtop_flags with + match !ideslave_coqtop_flags with | None -> None | Some s -> let open Str in diff --git a/ide/coq.mli b/ide/coq.mli index 463dd134a4..8c4727b37d 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -171,3 +171,6 @@ val check_connection : string list -> unit val interrupter : (int -> unit) ref val save_all : (unit -> unit) ref + +(* Flags to be used for ideslave *) +val ideslave_coqtop_flags : string option ref diff --git a/ide/coqide.ml b/ide/coqide.ml index 3cc46b6aa5..4de9a5288f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1360,7 +1360,7 @@ let read_coqide_args argv = Backtrace.record_backtrace true; filter_coqtop coqtop project_files ("-debug"::out) args |"-coqtop-flags" :: flags :: args-> - Flags.ideslave_coqtop_flags := Some flags; + Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files out args |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg -> (* argument added by MacOS during .app launch *) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 6d1064d25f..fe86df0847 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -458,8 +458,9 @@ 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 doc = - set_doc doc; +let loop _args ~state = + let open Vernac.State in + set_doc state.doc; init_signal_handler (); catch_break := false; let in_ch, out_ch = Spawned.get_channels () in diff --git a/ide/minilib.ml b/ide/minilib.ml index 2b278fac69..572222c069 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -20,7 +20,7 @@ type level = [ | `FATAL ] (** Some excerpt of Util and similar files to avoid loading the whole - module and its dependencies (and hence Compat and Camlp4) *) + module and its dependencies (and hence Compat and Camlp5) *) let debug = ref false diff --git a/ide/minilib.mli b/ide/minilib.mli index c96e59b226..4f5fbe7db7 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -7,7 +7,7 @@ (***********************************************************************) (** Some excerpts of Util and similar files to avoid depending on them - and hence on Compat and Camlp4 *) + and hence on Compat and Camlp5 *) val print_list : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit |