Adding methods help and parse_extra to custom toplevels data.

In particular, method init does not do parsing any more.

This allows for instance to let coqidetop treats itself the
"-filteropts" option.

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