From a6f5008e7976e8598556a5547ebe2f5e8e35d688 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Mon, 24 Feb 2025 13:13:16 +0100
Subject: [PATCH] feat: add vscoq/interrupt verb to language server

WIP
---
 language-server/protocol/extProtocol.ml | 2 ++
 language-server/vscoqtop/lspManager.ml  | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index ca863b134..c848ef4f8 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -60,6 +60,7 @@ module Notification = struct
     | InterpretToPoint of InterpretToPointParams.t
     | StepForward of StepForwardParams.t
     | StepBackward of StepBackwardParams.t
+    | Interrupt
 
     let of_jsonrpc (Jsonrpc.Notification.{ method_; params } as notif) =
       let open Lsp.Import.Result.O in
@@ -76,6 +77,7 @@ module Notification = struct
       | "vscoq/interpretToEnd" ->
         let+ params = Lsp.Import.Json.message_params params InterpretToEndParams.t_of_yojson in
         InterpretToEnd params
+      | "vscoq/interrupt" -> Ok Interrupt
       | _ ->
         let+ notif = Lsp.Client_notification.of_jsonrpc notif in
         Std notif 
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index ff84ecf0b..904ebc21e 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -535,6 +535,8 @@ let workspaceDidChangeConfiguration params =
   | Continuous -> run_documents ()
   | Manual -> reset_observe_ids (); ([] : events)
 
+let handle_interrupt () = []
+
 let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a, error) result * events =
   fun id req ->
   match req with
@@ -590,6 +592,7 @@ let dispatch_notification =
   | InterpretToEnd params -> log (fun () -> "Received notification: vscoq/interpretToEnd"); coqtopInterpretToEnd params
   | StepBackward params -> log (fun () -> "Received notification: vscoq/stepBackward"); coqtopStepBackward params
   | StepForward params -> log (fun () -> "Received notification: vscoq/stepForward"); coqtopStepForward params
+  | Interrupt -> log (fun () -> "Received notification: vscoq/interrupt"); handle_interrupt ()
   | Std notif -> dispatch_std_notification notif
 
 let handle_lsp_event = function