[stm] [flags] Move document mode flags to the STM.

We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.

Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.

In particular:

== Added flags ==

- `Safe_typing.allow_delayed_constants`
  Allow delayed constants in the kernel.

- `Flags.record_aux_file`
  Output `Proof using` information from the kernel.

- `System.trust_file_cache`
  Assume that the file system won't change during our run.

== Deleted flags ==

- `Flags.compilation_mode`
- `Flags.batch_mode`

Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.

The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.

1 files changed, 20 insertions, 3 deletions

diff --git a/stm/stm.mli b/stm/stm.mli
index 3f01fca01..ea8aecaed 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -10,6 +10,26 @@ open Names
 
 (** state-transaction-machine interface *)
 
+(** The STM doc type determines some properties such as what
+    uncompleted proofs are allowed and recording of aux files. *)
+type stm_doc_type =
+  | VoDoc       of DirPath.t
+  | VioDoc      of DirPath.t
+  | Interactive of DirPath.t
+
+(* Main initalization routine *)
+type stm_init_options = {
+  doc_type     : stm_doc_type;
+(*
+  fb_handler   : Feedback.feedback -> unit;
+  iload_path   : (string list * string * bool) list;
+  require_libs : (Names.DirPath.t * string * bool option) list;
+  implicit_std : bool;
+*)
+}
+
+val init : stm_init_options -> unit
+
 (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
 val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
@@ -83,9 +103,6 @@ val finish_tasks : string ->
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
 
-(* Misc *)
-val init : unit -> unit
-
 (* This returns the node at that position *)
 val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option