Interleave commandline require/set/unset commands

2 files changed, 75 insertions, 14 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 5790bfc07e..b296f8f08f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2576,6 +2576,21 @@ end (* }}} *)
 (******************************************************************************)
 
 (** STM initialization options: *)
+
+type option_command = OptionSet of string option | OptionUnset
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  (* -load-vernac-source interleaving is not supported yet *)
+  (* | LoadInjection of (string * bool) *)
+
 type stm_init_options =
   { doc_type : stm_doc_type
   (** The STM does set some internal flags differently depending on
@@ -2589,12 +2604,9 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; require_libs : (string * string option * bool option) list
-  (** Require [require_libs] before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+  ; injections : injection_command list
+  (** Injects Require and Set/Unset commands before the initial
+     state is ready *)
 
   ; stm_options  : AsyncOpts.stm_opt
   (** Low-level STM options *)
@@ -2625,13 +2637,51 @@ let dirpath_of_file f =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } =
+let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
 
   let require_file (dir, from, exp) =
     let mp = Libnames.qualid_of_string dir in
     let mfrom = Option.map Libnames.qualid_of_string from in
     Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
 
+  let interp_set_option opt v old =
+    let open Goptions in
+    let err expect =
+      let opt = String.concat " " opt in
+      let got = v in (* avoid colliding with Pp.v *)
+      CErrors.user_err
+        Pp.(str "-set: " ++ str opt ++
+            str" expects " ++ str expect ++
+            str" but got " ++ str got)
+    in
+    match old with
+    | BoolValue _ ->
+      let v = match String.trim v with
+        | "true" -> true
+        | "false" | "" -> false
+        | _ -> err "a boolean"
+      in
+      BoolValue v
+    | IntValue _ ->
+      let v = String.trim v in
+      let v = match int_of_string_opt v with
+        | Some _ as v -> v
+        | None -> if v = "" then None else err "an int"
+      in
+      IntValue v
+    | StringValue _ -> StringValue v
+    | StringOptValue _ -> StringOptValue (Some v) in
+
+  let set_option = let open Goptions in function
+      | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
+      | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
+      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in
+
+  let handle_injection = function
+    | RequireInjection r -> require_file r
+    (* | LoadInjection l -> *)
+    | OptionInjection o -> set_option o in
+
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
 
@@ -2670,7 +2720,7 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options }
   end;
 
   (* Import initial libraries. *)
-  List.iter require_file require_libs;
+  List.iter handle_injection injections;
 
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/stm/stm.mli b/stm/stm.mli
index 2c27d63b82..9780c96512 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -52,6 +52,20 @@ type stm_doc_type =
   | VioDoc      of string       (* file path *)
   | Interactive of interactive_top    (* module path *)
 
+type option_command = OptionSet of string option | OptionUnset
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  (* -load-vernac-source interleaving is not supported yet *)
+  (* | LoadInjection of (string * bool) *)
+
 (** STM initialization options: *)
 type stm_init_options =
   { doc_type : stm_doc_type
@@ -66,12 +80,9 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; require_libs : (string * string option * bool option) list
-  (** Require [require_libs] before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+  ; injections : injection_command list
+  (** Injects Require and Set/Unset commands before the initial
+     state is ready *)
 
   ; stm_options  : AsyncOpts.stm_opt
   (** Low-level STM options *)