aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-01-08 21:28:08 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-31 06:58:25 +0200
commit20437f77f889a544e66a266407f34a4137e8a47c (patch)
tree63c2888d47f39a650ea2068956b500b3c04f0020 /stm
parent2d2d16430822f1768ce4f3c62ef0750b94e4747f (diff)
[doc] Add some more documentation to STM API.
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.mli36
1 files changed, 25 insertions, 11 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index a8eb10fb3..7a720aa72 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -39,14 +39,25 @@ module AsyncOpts : sig
end
-(** The STM doc type determines some properties such as what
- uncompleted proofs are allowed and recording of aux files. *)
+(** The STM document type [stm_doc_type] determines some properties
+ such as what uncompleted proofs are allowed and what gets recorded
+ to aux files. *)
type stm_doc_type =
- | VoDoc of string
- | VioDoc of string
- | Interactive of DirPath.t
+ | VoDoc of string (* file path *)
+ | VioDoc of string (* file path *)
+ | Interactive of DirPath.t (* module path *)
-(* Main initalization routine *)
+(** Coq initalization options:
+
+ - [doc_type]: Type of document being created.
+
+ - [require_libs]: list of libraries/modules to be pre-loaded at
+ startup. A tuple [(modname,modfrom,import)] is equivalent to [From
+ modfrom Require modname]; [import] works similarly to
+ [Library.require_library_from_dirpath], [Some false] will import
+ the module, [Some true] will additionally export it.
+
+*)
type stm_init_options = {
(* The STM will set some internal flags differently depending on the
specified [doc_type]. This distinction should dissappear at some
@@ -72,12 +83,14 @@ type stm_init_options = {
(** The type of a STM document *)
type doc
+(** [init_core] performs some low-level initalization; should go away
+ in future releases. *)
val init_core : unit -> unit
-(* Starts a new document *)
+(** [new_doc opt] Creates a new document with options [opt] *)
val new_doc : stm_init_options -> doc * Stateid.t
-(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
+(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
state [sid] Returns [End_of_input] if the stream ends *)
val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
Vernacexpr.vernac_control CAst.t
@@ -115,14 +128,15 @@ val query : doc:doc ->
type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
-(* Evaluates the tip of the current branch *)
+(* [observe doc sid]] Check / execute span [sid] *)
+val observe : doc:doc -> Stateid.t -> doc
+
+(* [finish doc] Fully checks a document up to the "current" tip. *)
val finish : doc:doc -> doc
(* Internal use (fake_ide) only, do not use *)
val wait : doc:doc -> doc
-val observe : doc:doc -> Stateid.t -> doc
-
val stop_worker : string -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)