[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, 6 insertions, 0 deletions

diff --git a/lib/system.mli b/lib/system.mli
index 7281de97c..aa964abeb 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -54,6 +54,12 @@ val where_in_path_rex :
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
+val trust_file_cache : bool ref
+(** [trust_file_cache] indicates whether we trust the underlying
+    mapped file-system not to change along the execution of Coq. This
+    assumption greatly speds up file search, but it is often
+    inconvenient in interactive mode *)
+
 val file_exists_respecting_case : string -> string -> bool
 
 (** {6 I/O functions } *)