diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | ide/idetop.ml | 23 |
2 files changed, 19 insertions, 6 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 92c24b3b85..889cc3be36 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -102,7 +102,7 @@ let display_coqtop_answer cmd lines = let rec filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^" -nois -batch " ^ argstr in let cmd = requote cmd in let filtered_args = ref [] in let errlines = ref [] in diff --git a/ide/idetop.ml b/ide/idetop.ml index c6a8fdaa55..c7638343b0 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -553,12 +553,25 @@ 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 islave_parse ~opts extra_args = + let open Coqtop in + let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in + let extra_args = parse extra_args in + (* One of the role of coqidetop is to find the name of buffers to open *) + (* in the command line; Coqide is waiting these names on stdout *) + (* (see filter_coq_opts in coq.ml), so we send them now *) + print_string (String.concat "\n" extra_args); + run_mode, [] + +let islave_init ~opts = + CoqworkmgrApi.(init High) let () = let open Coqtop in - let custom = { init = islave_init; run = loop; opts = Coqargs.default } in + let custom = { + parse_extra = islave_parse ; + help = (fun _ -> output_string stderr "Same options as coqtop"); + init = islave_init; + run = loop; + opts = Coqargs.default } in start_coq custom |