aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorEnrico Tassi2021-01-05 11:34:35 +0100
committerEnrico Tassi2021-01-27 09:45:49 +0100
commit4264aec518d5407f345c58e18e014e15e9ae96af (patch)
tree03209892ae2549f171af39efa5d6925b745d54ec /ide
parent4390b6907b3d07793c2e8f9e7ad3cc38d9488711 (diff)
[sysinit] new component for system initialization
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide/idetop.ml16
1 files changed, 6 insertions, 10 deletions
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 528e2a756b..ed0eb8f34b 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -513,7 +513,7 @@ 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 run_mode ~opts:_ state =
+let loop (run_mode,_) ~opts:_ state =
match run_mode with
| Coqtop.Batch -> exit 0
| Coqtop.Interactive ->
@@ -582,23 +582,19 @@ coqidetop specific options:\n\
let islave_parse ~opts extra_args =
let open Coqtop in
- let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in
+ let (run_mode, stm_opts), 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, []
+ (run_mode, stm_opts), []
-let islave_init run_mode ~opts =
+let islave_init (run_mode, stm_opts) ~opts =
if run_mode = Coqtop.Batch then Flags.quiet := true;
- Coqtop.init_toploop opts
+ Coqtop.init_toploop opts stm_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 islave_default_opts = Coqargs.default
let () =
let open Coqtop in