Merge pull request #734 from coq-community/nav-commands-continuous-mode

Add api for step navigation in continuous mode.
coq · Feb 16, 2024 · 794b3b4 · 794b3b4
2 parents a1b0323 + 74b3764
commit 794b3b4
Show file tree

Hide file tree

Showing 6 changed files with 94 additions and 30 deletions.
diff --git a/client/package.json b/client/package.json
@@ -289,14 +289,12 @@
       {
         "command": "extension.coq.stepForward",
         "title": "Step Forward",
-        "category": "Coq",
-        "enablement": "config.vscoq.proof.mode == 0"
+        "category": "Coq"
       },
       {
         "command": "extension.coq.stepBackward",
         "title": "Step Backward",
-        "category": "Coq",
-        "enablement": "config.vscoq.proof.mode == 0"
+        "category": "Coq"
       },
       {
         "command": "extension.coq.documentState",

diff --git a/client/src/extension.ts b/client/src/extension.ts
@@ -175,8 +175,28 @@ export function activate(context: ExtensionContext) {
         registerVscoqTextCommand('expandAllQueries', () => searchProvider.expandAll());
         registerVscoqTextCommand('interpretToPoint', (editor) => sendInterpretToPoint(editor, client));
         registerVscoqTextCommand('interpretToEnd', (editor) => sendInterpretToEnd(editor, client));
-        registerVscoqTextCommand('stepForward', (editor) => sendStepForward(editor, client));
-        registerVscoqTextCommand('stepBackward', (editor) => sendStepBackward(editor, client));
+        registerVscoqTextCommand('stepForward', (editor) => {
+
+            if(workspace.getConfiguration('vscoq.proof').mode === 1) {
+                const textDocument = makeVersionedDocumentId(editor);
+                const position = editor.selection.active;
+                client.sendNotification("vscoq/stepForward", {textDocument: textDocument, position: position});
+            }
+            else {
+                sendStepForward(editor, client);
+            }
+
+        });
+        registerVscoqTextCommand('stepBackward', (editor) => {
+            if(workspace.getConfiguration('vscoq.proof').mode === 1) {
+                const textDocument = makeVersionedDocumentId(editor);
+                const position = editor.selection.active;
+                client.sendNotification("vscoq/stepBackward", {textDocument: textDocument, position: position});
+            }
+            else {
+                sendStepBackward(editor, client);
+            }
+        });
         registerVscoqTextCommand('documentState', async (editor) => {
 
             documentStateProvider.setDocumentUri(editor.document.uri);
@@ -208,8 +228,8 @@ export function activate(context: ExtensionContext) {
             const editors = window.visibleTextEditors.filter(editor => {
                 return editor.document.uri.toString() === uri.toString();
             });
-            if(workspace.getConfiguration('vscoq.proof.cursor').sticky === true &&
-            workspace.getConfiguration('vscoq.proof').mode === 0) {
+            if(workspace.getConfiguration('vscoq.proof.cursor').sticky === true ||
+            workspace.getConfiguration('vscoq.proof').mode === 1) {
                 editors.map(editor => {
                     editor.selections = [new Selection(range.end, range.end)];
                     editor.revealRange(range, TextEditorRevealType.Default);

diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
@@ -201,6 +201,28 @@ let interpret_to_position st pos =
   | None -> (st, []) (* document is empty *)
   | Some id -> interpret_to st id
 
+let get_next_range st pos =
+  match id_of_pos st pos with
+  | None -> None
+  | Some id ->
+    match Document.get_sentence st.document id with
+    | None -> None
+    | Some { stop } ->
+      match Document.find_sentence_after st.document (stop+1) with
+      | None -> Some (Document.range_of_id st.document id)
+      | Some { id } -> Some (Document.range_of_id st.document id)
+
+let get_previous_range st pos =
+  match id_of_pos st pos with
+  | None -> None
+  | Some id ->
+    match Document.get_sentence st.document id with
+    | None -> None
+    | Some { start } ->
+      match Document.find_sentence_before st.document (start) with
+      | None -> Some (Document.range_of_id st.document id)
+      | Some { id } -> Some (Document.range_of_id st.document id)
+
 let interpret_to_previous st =
   match st.observe_id with
   | None -> failwith "interpret to previous with no observe_id"

diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
@@ -48,6 +48,12 @@ val clear_observe_id : state -> state
 val reset_to_top : state -> state
 (** [reset_to_top state] updates the state to make the observe_id Top *)
 
+val get_next_range : state -> Position.t -> Range.t option
+(** [get_next_range st pos] get the range of the next sentence relative to pos *)
+
+val get_previous_range : state -> Position.t -> Range.t option
+(** [get_previous_pos st pos] get the range of the previous sentence relative to pos *)
+
 val interpret_to_position : state -> Position.t -> (state * events)
 (** [interpret_to_position stateful doc pos] navigates to the last sentence ending
     before or at [pos] and returns the resulting state. The [stateful] flag 

diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
@@ -40,6 +40,7 @@ module Notification = struct
 
       type t = {
         textDocument : VersionedTextDocumentIdentifier.t;
+        position: Position.t option;
       } [@@deriving yojson]
 
     end
@@ -48,6 +49,7 @@ module Notification = struct
 
       type t = {
         textDocument : VersionedTextDocumentIdentifier.t;
+        position: Position.t option;
       } [@@deriving yojson]
 
     end

diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
@@ -311,34 +311,50 @@ let coqtopInterpretToPoint params =
     sel_events @ [ mk_proof_view_event uri (Some position)]
 
 let coqtopStepBackward params =
-  let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in
+  let Notification.Client.StepBackwardParams.{ textDocument = { uri }; position } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log "[stepForward] ignoring event on non existant document"; []
+  | None -> log "[stepBackward] ignoring event on non existant document"; []
   | Some st ->
-    let (st, events) = Dm.DocumentManager.interpret_to_previous st in
-    let range = Dm.DocumentManager.observe_id_range st in
-    Hashtbl.replace states (DocumentUri.to_path uri) st;
-    update_view uri st;
-    match range with
-    | None ->
-      inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
-    | Some range ->
-      [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+    if !check_mode = Settings.Mode.Continuous then
+      match position with
+      | None -> []
+      | Some pos -> 
+        match Dm.DocumentManager.get_previous_range st pos with
+        | None -> []
+        | Some range -> [mk_move_cursor_event uri range]
+    else
+      let (st, events) = Dm.DocumentManager.interpret_to_previous st in
+      let range = Dm.DocumentManager.observe_id_range st in
+      Hashtbl.replace states (DocumentUri.to_path uri) st;
+      update_view uri st;
+      match range with
+      | None ->
+        inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+      | Some range ->
+        [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
 
 let coqtopStepForward params =
-  let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in
+  let Notification.Client.StepForwardParams.{ textDocument = { uri }; position } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log "[stepBackward] ignoring event on non existant document"; []
+  | None -> log "[stepForward] ignoring event on non existant document"; []
   | Some st ->
-    let (st, events) = Dm.DocumentManager.interpret_to_next st in
-    let range = Dm.DocumentManager.observe_id_range st in
-    Hashtbl.replace states (DocumentUri.to_path uri) st;
-    update_view uri st;
-    match range with 
-    | None ->
-      inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
-    | Some range -> 
-      [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+    if !check_mode = Settings.Mode.Continuous then
+      match position with
+      | None -> []
+      | Some pos -> 
+        match Dm.DocumentManager.get_next_range st pos with
+        | None -> []
+        | Some range -> [mk_move_cursor_event uri range]
+    else
+      let (st, events) = Dm.DocumentManager.interpret_to_next st in
+      let range = Dm.DocumentManager.observe_id_range st in
+      Hashtbl.replace states (DocumentUri.to_path uri) st;
+      update_view uri st;
+      match range with 
+      | None ->
+        inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+      | Some range ->
+        [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
 
   let make_CompletionItem i item : CompletionItem.t = 
     let (label, insertText, typ, path) = Dm.CompletionItems.pp_completion_item item in