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.

1 files changed, 7 insertions, 2 deletions

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