diff --git a/CHANGES.md b/CHANGES.md index 8374055e..5410dd87 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -75,6 +75,9 @@ - new VSCode commands to allow to move one sentence backwards / forward, this is particularly useful when combined with lazy checking mode (@ejgallego, #671, fixes #263, fixes #580) + - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious` + are now bound by default to `Alt + N` / `Alt + P` keybindings + (@ejgallego, #718) - change diagnostic `extra` field to `data`, so we now conform to the LSP spec, include the data only when the `send_diags_extra_data` server-side option is enabled (@ejgallego, #670) @@ -135,8 +138,11 @@ the scheduler for the visible area of the document; combined with the new lazy checking mode, this provides checking on scroll, a feature inspired from Isabelle IDE (@ejgallego, #717) - - Have VSCode wait for full LSP client shutdown on server restart + - Have VSCode wait for full LSP client shutdown on server + restart. This fixes some bugs on extension restart (finally!) (@ejgallgo, #719) + - Center the view if cursor goes out of scope in + `sentenceNext/sentencePrevious` (@ejgallego, #718) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/editor/code/package.json b/editor/code/package.json index 45901146..0511545e 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -111,7 +111,7 @@ "title": "Coq LSP: try to jump to next Coq sentence" }, { - "command": "coq-lsp.sentenceBack", + "command": "coq-lsp.sentencePrevious", "title": "Coq LSP: try to jump to previous Coq sentence" }, { @@ -125,6 +125,18 @@ "key": "alt+enter", "mac": "meta+enter", "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)" + }, + { + "command": "coq-lsp.sentenceNext", + "key": "Alt+N", + "mac": "cmd+N", + "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)" + }, + { + "command": "coq-lsp.sentencePrevious", + "key": "Alt+P", + "mac": "cmd+P", + "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)" } ], "viewsContainers": { diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 6c3f2383..e0efc9c7 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -45,7 +45,7 @@ import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config"; import { InfoPanel, goalReq } from "./goals"; import { FileProgressManager } from "./progress"; import { coqPerfData, PerfDataView } from "./perf"; -import { sentenceNext, sentenceBack } from "./edit"; +import { sentenceNext, sentencePrevious } from "./edit"; import { HeatMap, HeatMapConfig } from "./heatmap"; import { debounce, throttle } from "throttle-debounce"; @@ -461,7 +461,7 @@ export function activateCoqLSP( coqEditorCommand("save", saveDocument); coqEditorCommand("sentenceNext", sentenceNext); - coqEditorCommand("sentenceBack", sentenceBack); + coqEditorCommand("sentencePrevious", sentencePrevious); coqEditorCommand("heatmap.toggle", heatMapToggle); diff --git a/editor/code/src/edit.ts b/editor/code/src/edit.ts index e01c64a2..c537a6ec 100644 --- a/editor/code/src/edit.ts +++ b/editor/code/src/edit.ts @@ -1,7 +1,23 @@ // Edition facilities for Coq files -import { TextEditor, Position, Range, Selection } from "vscode"; +import { + TextEditor, + Position, + Range, + Selection, + TextEditorRevealType, +} from "vscode"; -export function sentenceBack(editor: TextEditor) { +function setSelection(editor: TextEditor, newCursor: Position) { + editor.selection = new Selection(newCursor, newCursor); + + // Is there not a better way? + editor.revealRange( + new Range(newCursor, newCursor), + TextEditorRevealType.InCenterIfOutsideViewport + ); +} + +export function sentencePrevious(editor: TextEditor) { // Slice from the beginning of the document let cursor = editor.selection.active; let range = new Range(editor.document.positionAt(0), cursor); @@ -19,7 +35,7 @@ export function sentenceBack(editor: TextEditor) { index = text.lastIndexOf(match) + match.length; } let newCursor = editor.document.positionAt(index); - editor.selection = new Selection(newCursor, newCursor); + setSelection(editor, newCursor); } } @@ -40,6 +56,6 @@ export function sentenceNext(editor: TextEditor) { let newCursor = editor.document.positionAt( editor.document.offsetAt(cursor) + index ); - editor.selection = new Selection(newCursor, newCursor); + setSelection(editor, newCursor); } } diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md index c51f5bdc..eeaa51e2 100644 --- a/etc/doc/USER_MANUAL.md +++ b/etc/doc/USER_MANUAL.md @@ -46,8 +46,12 @@ facilities. In VSCode, these settings can be usually displayed in the ### Goal display By default, `coq-lsp` will follow cursor and show goals at cursor -position. This can be tweaked in options. There are commands to move -one Coq sentence forward / backwards. +position. This can be tweaked in options. + +The `coq-lsp.sentenceNext` and `coq-lsp.sentencePrevious` commands will +try to move the cursor one Coq sentence forward / backwards. These +commands are bound by default to `Alt + N` / `Alt + P` (`Cmd` on +MacOS). ### Incremental proof edition