From e43c35ba795520fe111ac39a834f334753491b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Apr 2017 10:31:29 +0200 Subject: [STM] explicit handling of parsing states DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès Co-authored-by: Emilio Jesus Gallego Arias --- stm/stm.mli | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index b6071fa56b..821ab59a43 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -93,16 +93,17 @@ val init_core : unit -> unit (** [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 - state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t -> - Vernacexpr.vernac_control CAst.t +(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state + [sid] and non terminal [entry]. [entry] receives in input the current proof + mode. [sid] should be associated with a valid parsing state (which may not + be the case if an error was raised at parsing time). *) +val parse_sentence : + doc:doc -> Stateid.t -> + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a (* Reminder: A parsable [pa] is constructed using [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) -exception End_of_input - (* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of the state [ontop]. The [ontop] parameter just asserts that the GUI is on -- cgit v1.2.3