[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 <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

1 files changed, 8 insertions, 5 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 716a942d5c..f91aa569d4 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -83,7 +83,10 @@ let set_doc doc = ide_doc := Some doc
 let add ((s,eid),(sid,verbose)) =
   let doc = get_doc () in
   let pa = Pcoq.Parsable.make (Stream.of_string s) in
-  let loc_ast = Stm.parse_sentence ~doc sid pa in
+  match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
+  | None -> assert false (* s is not an empty string *)
+  | Some (loc, ast) ->
+  let loc_ast = CAst.make ~loc ast in
   let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
   set_doc doc;
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
@@ -121,10 +124,10 @@ let query (route, (s,id)) =
 
 let annotate phrase =
   let doc = get_doc () in
-  let {CAst.loc;v=ast} =
-    let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
-    Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
-  in
+  let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
+  match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
+  | None -> Richpp.richpp_of_pp 78 (Pp.mt ())
+  | Some (_, ast) ->
   (* XXX: Width should be a parameter of annotate... *)
   Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)