[wip] Allow command to process several Coq commands.

controller/rq_goals.ml

@@ -31,20 +31,25 @@ let pp ~pp_format pp =
   | Pp -> Lsp.JCoq.Pp.to_yojson pp
   | Str -> `String (Pp.string_of_ppcmds pp)
 
-let parse ~token ~loc tac st =
-  let str = Gramlib.Stream.of_string tac in
-  let str = Coq.Parsing.Parsable.make ?loc str in
-  Coq.Parsing.parse ~token ~st str
-
-let parse_and_execute_in ~token ~loc tac st =
+(* TODO, what to do with feedback, what to do with errors *)
+let rec parse_execute_loop ~token pa st =
   let open Coq.Protect.E.O in
-  let* ast = parse ~token ~loc tac st in
+  let* ast = Coq.Parsing.parse ~token ~st pa in
   match ast with
-  | Some ast -> Fleche.Memo.Interp.eval ~token (st, ast)
+  | Some ast -> (
+    match Fleche.Memo.Interp.eval ~token (st, ast) with
+    | Coq.Protect.E.{ r = Coq.Protect.R.Completed (Ok st); feedback = _ } ->
+      parse_execute_loop ~token pa st
+    | res -> res)
   (* On EOF we return the previous state, the command was the empty string or a
      comment *)
   | None -> Coq.Protect.E.ok st
 
+let parse_and_execute_in ~token ~loc tac st =
+  let str = Gramlib.Stream.of_string tac in
+  let pa = Coq.Parsing.Parsable.make ?loc str in
+  parse_execute_loop ~token pa st
+
 let run_pretac ~token ~loc ~st pretac =
   match pretac with
   | None -> Coq.Protect.E.ok st

etc/doc/PROTOCOL.md

@@ -187,12 +187,19 @@ interface GoalRequest {
     textDocument: VersionedTextDocumentIdentifier;
     position: Position;
     pp_format?: 'Pp' | 'Str';
-    pretac?: string;
     command?: string;
     mode?: 'Prev' | 'After';
 }
 ```
 
+The first parameters are standard, `pp_format` controls the pretty
+printing format used in the results.
+
+The `command` parameter (experimental), is a list of Coq commands that
+will be run just _after_ `position` in `textDocument`, but _before_
+goals are sent to the user. This is often useful for ephemeral
+post-processing.
+
 Answer to the request is a `Goal[]` object, where
 
 ```typescript