From dd15e030be5e55d3770d27fbbc2fe0f5384f0166 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 May 2019 19:42:08 +0200
Subject: 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.
---
 ide/coq.ml    |  2 +-
 ide/idetop.ml | 23 ++++++++++++++++++-----
 2 files changed, 19 insertions(+), 6 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3


From 2bdfddc39d1fd6200042ddb95ded98b44e14b8e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 May 2019 11:24:51 +0200
Subject: Passing command-line option async_proofs_worker_priority
 functionally.

We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
---
 ide/idetop.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index c7638343b0..f39c59f5d8 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -563,8 +563,13 @@ let islave_parse ~opts extra_args =
   print_string (String.concat "\n" extra_args);
   run_mode, []
 
-let islave_init ~opts =
-  CoqworkmgrApi.(init High)
+let islave_init ~opts = ()
+
+let islave_default_opts =
+  Coqargs.{ default with
+    config = { default.config with
+      stm_flags = { default.config.stm_flags with
+         Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}}
 
 let () =
   let open Coqtop in
@@ -573,5 +578,5 @@ let () =
       help = (fun _ -> output_string stderr "Same options as coqtop");
       init = islave_init;
       run = loop;
-      opts = Coqargs.default } in
+      opts = islave_default_opts } in
   start_coq custom
-- 
cgit v1.2.3


From 01c965e1989cbc528d46b1751d8c2c708542da4e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 May 2019 20:26:30 +0200
Subject: Some common points between coqc and other coq binaries.

- Binding coqc execution to the generic support for Coq binaries
  (i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
  can avoid to call it. By the way, it is unclear what workerloop
  should do with it. Also, it is unclear how much the -l option should
  be considered an coqidetop or coq*worker option. In any case, it
  should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
  phase. Seems ok, despites the few involved side effects.
---
 ide/idetop.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index f39c59f5d8..f79ad5deab 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -496,7 +496,10 @@ 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 ~opts:_ ~state =
+let loop run_mode ~opts:_ state =
+  match run_mode with
+  | Coqtop.Batch -> exit 0
+  | Coqtop.Interactive ->
   let open Vernac.State in
   set_doc state.doc;
   init_signal_handler ();
@@ -563,7 +566,9 @@ let islave_parse ~opts extra_args =
   print_string (String.concat "\n" extra_args);
   run_mode, []
 
-let islave_init ~opts = ()
+let islave_init run_mode ~opts =
+  if run_mode = Coqtop.Batch then Flags.quiet := true;
+  Coqtop.init_toploop opts
 
 let islave_default_opts =
   Coqargs.{ default with
-- 
cgit v1.2.3


From fe487e8eaae3186803ec657c517d0ebebab3bafd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 May 2019 22:42:48 +0200
Subject: An even more uniform treatment of the -help option across
 executables.

Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.
---
 ide/idetop.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index f79ad5deab..eb76951b44 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -552,8 +552,10 @@ let rec parse = function
        x :: parse rest
   | [] -> []
 
-let () = Usage.add_to_usage "coqidetop"
-"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
+let () = Usage.add_to_usage "coqidetop" "" "\n\
+coqidetop specific options:\n\
+\n  --xml_formatinclude dir           (idem)\
+\n  --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_parse ~opts extra_args =
@@ -580,7 +582,7 @@ let () =
   let open Coqtop in
   let custom = {
       parse_extra = islave_parse ;
-      help = (fun _ -> output_string stderr "Same options as coqtop");
+      help = Usage.print_usage "coqidetop";
       init = islave_init;
       run = loop;
       opts = islave_default_opts } in
-- 
cgit v1.2.3


From f2779d48d3b7735687444e22b16cdb7cb8f7ce60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 May 2019 09:36:57 +0200
Subject: Usage: bypassing a useless detour via a reference.

---
 ide/idetop.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index eb76951b44..02682e2ee9 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -552,11 +552,15 @@ let rec parse = function
        x :: parse rest
   | [] -> []
 
-let () = Usage.add_to_usage "coqidetop" "" "\n\
+let coqidetop_specific_usage = Usage.{
+  executable_name = "coqidetop";
+  extra_args = "";
+  extra_options = "\n\
 coqidetop specific options:\n\
 \n  --xml_formatinclude dir           (idem)\
 \n  --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_parse ~opts extra_args =
   let open Coqtop in
@@ -582,7 +586,7 @@ let () =
   let open Coqtop in
   let custom = {
       parse_extra = islave_parse ;
-      help = Usage.print_usage "coqidetop";
+      help = coqidetop_specific_usage;
       init = islave_init;
       run = loop;
       opts = islave_default_opts } in
-- 
cgit v1.2.3