[stm] Move main parsing entry point to the STM.

Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.

This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.

This commit supersedes PR#204.

2 files changed, 97 insertions, 74 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index f8d959f97..fb0a0514d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -93,49 +93,6 @@ let may_pierce_opaque = function
   | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
   | _ -> false
 
-(* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let indentation_of_string s =
-  let len = String.length s in
-  let rec aux n i precise =
-    if i >= len then 0, precise, len
-    else
-      match s.[i] with
-      | ' ' | '\t' -> aux (succ n) (succ i) precise
-      | '\n' | '\r' -> aux 0 (succ i) true
-      | _ -> n, precise, len in
-  aux 0 0 false
-
-(* We must parse on top of a state id, it should be something like:
-
-   - get parsing information for that state.
-   - feed the parsable / parser with the right parsing information.
-   - call the parser
-
-   Now, the invariant in ensured by the callers, but this is a bit
-   problematic.
-*)
-let stm_parse ?(indlen_prev=fun() -> 0) s =
-  let indentation, precise, strlen = indentation_of_string s in
-  let indentation =
-    if precise then indentation else indlen_prev () + indentation in
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  Flags.with_option Flags.we_are_parsing (fun () ->
-    try
-      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
-      | None            -> raise (Invalid_argument "stm_parse")
-      | Some (loc, ast) -> indentation, strlen, loc, ast
-    with e when CErrors.noncritical e ->
-      let (e, info) = CErrors.push e in
-      (* This is the old error recovery strategy.             *)
-      (* let loc = Loc.get_loc info in                        *)
-      (* feedback (?newtip || eid) (Message(Error, loc, msg)) *)
-      iraise (e, info))
-  ()
-
-let pr_open_cur_subgoals () =
-  try Printer.pr_open_subgoals ()
-  with Proof_global.NoCurrentProof -> Pp.str ""
-
 let update_global_env () =
   if Proof_global.there_are_pending_proofs () then
     Proof_global.update_global_env ()
@@ -2385,6 +2342,10 @@ let observe id =
     VCS.restore vcs;
     iraise e
 
+let pr_open_cur_subgoals () =
+  try Printer.pr_open_subgoals ()
+  with Proof_global.NoCurrentProof -> Pp.str ""
+
 let finish ?(print_goals=false) () =
   let head = VCS.current_branch () in
   observe (VCS.get_branch_pos head);
@@ -2706,26 +2667,80 @@ let get_ast id =
 
 let stop_worker n = Slaves.cancel_worker n
 
+(* We must parse on top of a state id, it should be something like:
+
+   - get parsing information for that state.
+   - feed the parsable / parser with the right parsing information.
+   - call the parser
+
+   Now, the invariant in ensured by the callers, but this is a bit
+   problematic.
+*)
+exception End_of_input
+
+let parse_sentence sid pa =
+  (* XXX: Should this restore the previous state?
+     Using reach here to try to really get to the
+     proper state makes the error resilience code fail *)
+  (* Reach.known_state ~cache:`Yes sid; *)
+  let cur_tip = VCS.cur_tip () in
+  if not (Stateid.equal sid cur_tip) then
+    user_err ~hdr:"Stm.parse_sentence"
+      (str "Currently, the parsing api only supports parsing at the tip of the document.");
+  Flags.with_option Flags.we_are_parsing (fun () ->
+      try
+        match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+        | None     -> raise End_of_input
+        | Some com -> com
+      with e when CErrors.noncritical e ->
+        let (e, info) = CErrors.push e in
+        iraise (e, info))
+    ()
+
 (* You may need to know the len + indentation of previous command to compute
  * the indentation of the current one.
  *  Eg.   foo. bar.
  * Here bar is indented of the indentation of foo + its strlen (4) *)
-let ind_len_of id =
-  if Stateid.equal id Stateid.initial then 0
-  else match (VCS.visit id).step with
-  | `Cmd { ctac = true; cast = { indentation; strlen } } ->
-       indentation + strlen
-  | _ -> 0
-
-let add ~ontop ?newtip ?(check=ignore) verb s =
+let ind_len_loc_of_id sid =
+  if Stateid.equal sid Stateid.initial then None
+  else match (VCS.visit sid).step with
+  | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
+         Some (indentation, strlen, loc)
+  | _ -> None
+
+(* the indentation logic works like this: if the beginning of the
+   command is different than the start we are in a new line, thus
+   indentation follows from the starting position. Otherwise, we use
+   the previous one plus the offset.
+
+   Note, this could maybe improved by handling more cases in
+   compute_indentation. *)
+
+let compute_indentation sid loc =
+  let open Loc              in
+  (* The effective lenght is the lenght on the last line *)
+  let len = loc.ep - loc.bp in
+  let prev_indent = match ind_len_loc_of_id sid with
+    | None         -> 0
+    | Some (i,l,p) -> i + l
+  in
+  (* Now if the line has not changed, the need to add the previous indent *)
+  let eff_indent = loc.bp - loc.bol_pos in
+  if loc.bol_pos = 0 then
+    eff_indent + prev_indent, len
+  else
+    eff_indent, len
+
+
+let add ~ontop ?newtip verb (loc, ast) =
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
-    (* For now, arbitrary edits should be announced with edit_at *)
-    anomaly(str"Not yet implemented, the GUI should not try this");
-  let indentation, strlen, loc, ast =
-    stm_parse ~indlen_prev:(fun () -> ind_len_of ontop) s in
+    user_err ~hdr:"Stm.add"
+      (str "You used Stm.add on a different state than the tip" ++ fnl () ++
+       str "This is not supported yet, sorry.");
+  let indentation, strlen = compute_indentation ontop loc in
   CWarnings.set_current_loc loc;
-  check(loc,ast);
+  (* XXX: Classifiy vernac should be moved inside process transaction *)
   let clas = classify_vernac ast in
   let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
   match process_transaction ?newtip ~tty:false aast clas with
@@ -2744,7 +2759,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
-    let indentation, strlen, loc, ast = stm_parse s in
+    let loc, ast = parse_sentence at s in
+    let indentation, strlen = compute_indentation at loc in
     CWarnings.set_current_loc loc;
     let clas = classify_vernac ast in
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
diff --git a/stm/stm.mli b/stm/stm.mli
index d3e5dde39..a31e4289d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -13,24 +13,31 @@ open Loc
 
 (** state-transaction-machine interface *)
 
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop].
-   [check] is called on the AST.
-   The [ontop] parameter is just for asserting the GUI is on sync, but
-   will eventually call edit_at on the fly if needed.
-   The sentence [s] is parsed in the state [ontop].
-   If [newtip] is provided, then the returned state id is guaranteed to be
-   [newtip] *)
-val add :
-  ontop:Stateid.t -> ?newtip:Stateid.t ->
-  ?check:(vernac_expr located -> unit) ->
-  bool -> string ->
-    Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
-
-(* parses and executes a command at a given state, throws away its side effects
-   but for the printings.  Feedback is sent with report_with (defaults to dummy
-   state id)  *)
+(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
+   state [sid] Returns [End_of_input] if the stream ends *)
+val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
+  Vernacexpr.vernac_expr Loc.located
+
+(* Reminder: A parsable [pa] is constructed using
+   [Pcoq.Gram.coq_parsable 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
+   sync, but it will eventually call edit_at on the fly if needed.
+   If [newtip] is provided, then the returned state id is guaranteed
+   to be [newtip] *)
+val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
+  bool -> (Loc.t * Vernacexpr.vernac_expr) ->
+  Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
+   throwing away side effects except messages. Feedback will
+   be sent with [report_with], which defaults to the dummy state id *)
 val query :
-  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
+  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit
 
 (* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
    the requested id is the new document tip hence the document portion following