From a34c58404547ca59ef4c196fdc4eae3e50c53ee8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 18 Sep 2024 17:23:56 +0200
Subject: [PATCH] [wip] Allow `command` to process several Coq commands.

---
 controller/rq_goals.ml | 21 +++++++++++++--------
 etc/doc/PROTOCOL.md    |  9 ++++++++-
 2 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml
index fa1cb142..0ec2e7bf 100644
--- a/controller/rq_goals.ml
+++ b/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
diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md
index 6b167e77..4a77e4bf 100644
--- a/etc/doc/PROTOCOL.md
+++ b/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