[stm] [toplevel] Make loadpath a parameter of the document.

We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.

The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:

- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
  command line options, etc...

1 files changed, 16 insertions, 5 deletions

diff --git a/stm/stm.mli b/stm/stm.mli
index 8b5581979..8a4de34b4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -46,15 +46,26 @@ type stm_doc_type =
 
 (* Main initalization routine *)
 type stm_init_options = {
+  (* The STM will set some internal flags differently depending on the
+     specified [doc_type]. This distinction should dissappear at some
+     some point. *)
   doc_type     : stm_doc_type;
+
+  (* Initial load path in scope for the document. Usually extracted
+     from -R options / _CoqProject *)
+  iload_path   : Mltop.coq_path 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.  *)
   require_libs : (string * string option * bool option) list;
+
+  (* STM options that apply to the current document. *)
   stm_options  : AsyncOpts.stm_opt;
-(*
-  fb_handler   : Feedback.feedback -> unit;
-  iload_path   : (string list * string * bool) list;
-  implicit_std : bool;
-*)
 }
+(* fb_handler   : Feedback.feedback -> unit; *)
 
 (** The type of a STM document *)
 type doc