From 4264aec518d5407f345c58e18e014e15e9ae96af Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 Jan 2021 11:34:35 +0100
Subject: [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
---
 ide/coqide/idetop.ml | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

(limited to 'ide')

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


From 4c4d6cfacf92b555546055a45edc19b68245b83c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 14:19:59 +0100
Subject: [sysinit] move initialization code from coqtop to here

We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
---
 ide/coqide/idetop.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'ide')

diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index ed0eb8f34b..2941497c12 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -513,9 +513,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 (run_mode,_) ~opts:_ state =
+let loop ( { Coqtop.run_mode; color_mode },_) ~opts:_ state =
   match run_mode with
   | Coqtop.Batch -> exit 0
+  | Coqtop.Query_PrintTags -> Coqtop.print_style_tags color_mode; exit 0
   | Coqtop.Interactive ->
   let open Vernac.State in
   set_doc state.doc;
@@ -580,19 +581,19 @@ coqidetop specific options:\n\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
 }
 
-let islave_parse ~opts extra_args =
+let islave_parse extra_args =
   let open Coqtop in
-  let (run_mode, stm_opts), extra_args = coqtop_toplevel.parse_extra ~opts extra_args in
+  let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra 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, stm_opts), []
+  ( { Coqtop.run_mode; color_mode }, stm_opts), []
 
-let islave_init (run_mode, stm_opts) ~opts =
+let islave_init ( { Coqtop.run_mode; color_mode }, stm_opts) injections ~opts =
   if run_mode = Coqtop.Batch then Flags.quiet := true;
-  Coqtop.init_toploop opts stm_opts
+  Coqtop.init_toploop opts stm_opts injections
 
 let islave_default_opts = Coqargs.default
 
@@ -600,8 +601,8 @@ let () =
   let open Coqtop in
   let custom = {
       parse_extra = islave_parse ;
-      help = coqidetop_specific_usage;
-      init = islave_init;
+      usage = coqidetop_specific_usage;
+      init_extra = islave_init;
       run = loop;
-      opts = islave_default_opts } in
+      initial_args = islave_default_opts } in
   start_coq custom
-- 
cgit v1.2.3


From f5ec3f5cbd4bc2e0f65e1c52143b199ce7c2a5ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 17:13:59 +0100
Subject: [coqtop] handle -print-module-uid after initialization

---
 ide/coqide/idetop.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 2941497c12..b42c705add 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -516,7 +516,8 @@ let msg_format = ref (fun () ->
 let loop ( { Coqtop.run_mode; color_mode },_) ~opts:_ state =
   match run_mode with
   | Coqtop.Batch -> exit 0
-  | Coqtop.Query_PrintTags -> Coqtop.print_style_tags color_mode; exit 0
+  | Coqtop.(Query PrintTags) -> Coqtop.print_style_tags color_mode; exit 0
+  | Coqtop.(Query _) -> Printf.eprintf "Unknown query"; exit 1
   | Coqtop.Interactive ->
   let open Vernac.State in
   set_doc state.doc;
-- 
cgit v1.2.3