From 2fda0fc0725dd0b1a4560c8b8c2c0d9818912b1b Mon Sep 17 00:00:00 2001
From: diego <driverag22@gmail.com>
Date: Thu, 22 Dec 2022 13:01:08 +0100
Subject: [PATCH] added new vernac query with sentenceId, and used it to run
 coq commands on isolation

---
 .../processors/SerapiSearchProcessor.js       | 51 +++++++++++++------
 src/coq/serapi/util/SerapiCommandFactory.js   | 12 +++++
 2 files changed, 48 insertions(+), 15 deletions(-)

diff --git a/src/coq/serapi/processors/SerapiSearchProcessor.js b/src/coq/serapi/processors/SerapiSearchProcessor.js
index 174fd32a..0d2c37bd 100644
--- a/src/coq/serapi/processors/SerapiSearchProcessor.js
+++ b/src/coq/serapi/processors/SerapiSearchProcessor.js
@@ -2,7 +2,7 @@ import SerapiProcessor from '../util/SerapiProcessor';
 import {Mutex} from 'async-mutex';
 import {
   createCheckCommand, createQueryVernacCommand,
-  createSearchCommand,
+  createIndexedQueryVernacCommand, createSearchCommand,
 } from '../util/SerapiCommandFactory';
 import {COQ_EXCEPTION, parseErrorResponse} from '../SerapiParser';
 
@@ -217,20 +217,41 @@ class SerapiSearchProcessor extends SerapiProcessor {
    * @private
    */
   async _queryCommand(command) {
-    return this.sendCommand(createQueryVernacCommand(command), 'raw',
-        (feedback) => {
-          return {
-            result: feedback.string,
-          };
-        })
-        .then((result) => {
-          if (result.hasOwnProperty('result')) {
-            this.editor.message(result.result);
-          }
-          if (result.error) {
-            this.editor.message(result.errorMessage);
-          }
-        });
+    try {
+      return this.sendCommand(
+          createIndexedQueryVernacCommand(
+              command, this.state.idOfSentence(this.state.lastExecuted)), 'raw',
+          (feedback) => {
+            return {
+              result: feedback.string,
+            };
+          })
+          .then((result) => {
+            if (result.hasOwnProperty('result')) {
+              this.editor.message(result.result);
+            }
+            if (result.error) {
+              this.editor.message(result.errorMessage);
+            }
+          });
+    } catch (e) {
+      return this.sendCommand(
+          createQueryVernacCommand(
+              command), 'raw',
+          (feedback) => {
+            return {
+              result: feedback.string,
+            };
+          })
+          .then((result) => {
+            if (result.hasOwnProperty('result')) {
+              this.editor.message(result.result);
+            }
+            if (result.error) {
+              this.editor.message(result.errorMessage);
+            }
+          });
+    }
   }
 
   /**
diff --git a/src/coq/serapi/util/SerapiCommandFactory.js b/src/coq/serapi/util/SerapiCommandFactory.js
index 883b775a..6bde0ca4 100644
--- a/src/coq/serapi/util/SerapiCommandFactory.js
+++ b/src/coq/serapi/util/SerapiCommandFactory.js
@@ -68,6 +68,18 @@ export function createQueryVernacCommand(command) {
   return `(Query () (Vernac "${sanitise(command)}"))`;
 }
 
+/**
+ * Partial method for vernac commands to execute the command
+ * after a specific sentece
+ * @param {String} command the vernac commmand to execute
+ * @param {number} sentenceId the sentence id after which
+ * the command should execute
+ * @return {string} the command
+ */
+export function createIndexedQueryVernacCommand(command, sentenceId) {
+  return `(Query ((sid ${sentenceId})) (Vernac "${sanitise(command)}"))`;
+}
+
 /**
  * Create a serapi check command
  * @param {String} query the term to check for