feat: add vscoq/interrupt verb to language server

WIP
coq · Feb 24, 2025 · a6f5008 · a6f5008
1 parent 7883909
commit a6f5008
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git 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
@@ -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