feat: [lean4web] add option to change selectionMoveMove

leanprover · Jul 22, 2024 · 02af071 · 02af071
1 parent 0617371
commit 02af071
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 6 deletions.
diff --git a/vscode-lean4/src/abbreviation/AbbreviationFeature.ts b/vscode-lean4/src/abbreviation/AbbreviationFeature.ts
@@ -1,4 +1,4 @@
-import { AbbreviationProvider } from '@leanprover/unicode-input'
+import { AbbreviationProvider, SelectionMoveMode } from '@leanprover/unicode-input'
 import { Disposable, OutputChannel, languages } from 'vscode'
 import { AbbreviationHoverProvider } from './AbbreviationHoverProvider'
 import { AbbreviationRewriterFeature } from './AbbreviationRewriterFeature'
@@ -8,7 +8,7 @@ export class AbbreviationFeature {
     private readonly disposables = new Array<Disposable>()
     readonly abbreviations: AbbreviationProvider
 
-    constructor(outputChannel: OutputChannel) {
+    constructor(outputChannel: OutputChannel, selectionMoveMove?: SelectionMoveMode) {
         const config = new VSCodeAbbreviationConfig()
         this.disposables.push(config)
         this.abbreviations = new AbbreviationProvider(config)
@@ -18,7 +18,7 @@ export class AbbreviationFeature {
                 config.languages,
                 new AbbreviationHoverProvider(config, this.abbreviations),
             ),
-            new AbbreviationRewriterFeature(config, this.abbreviations, outputChannel),
+            new AbbreviationRewriterFeature(config, this.abbreviations, outputChannel, selectionMoveMove),
         )
     }
 

diff --git a/vscode-lean4/src/abbreviation/AbbreviationRewriterFeature.ts b/vscode-lean4/src/abbreviation/AbbreviationRewriterFeature.ts
@@ -1,5 +1,5 @@
-import { AbbreviationProvider } from '@leanprover/unicode-input'
-import { commands, Disposable, languages, OutputChannel, TextEditor, window, workspace } from 'vscode'
+import { AbbreviationProvider, SelectionMoveMode } from '@leanprover/unicode-input'
+import { Disposable, OutputChannel, TextEditor, commands, languages, window, workspace } from 'vscode'
 import { extUriEquals, toExtUri } from '../utils/exturi'
 import { VSCodeAbbreviationConfig } from './VSCodeAbbreviationConfig'
 import { VSCodeAbbreviationRewriter } from './VSCodeAbbreviationRewriter'
@@ -17,6 +17,7 @@ export class AbbreviationRewriterFeature {
         private readonly config: VSCodeAbbreviationConfig,
         private readonly abbreviationProvider: AbbreviationProvider,
         private readonly outputChannel: OutputChannel,
+        private readonly selectionMoveMove?: SelectionMoveMode,
     ) {
         void this.changedActiveTextEditor(window.activeTextEditor)
 
@@ -49,6 +50,7 @@ export class AbbreviationRewriterFeature {
                         abbreviationProvider,
                         outputChannel,
                         window.activeTextEditor,
+                        this.selectionMoveMove,
                     )
                 } else if (
                     this.activeAbbreviationRewriter !== undefined &&
@@ -86,6 +88,7 @@ export class AbbreviationRewriterFeature {
             this.abbreviationProvider,
             this.outputChannel,
             activeTextEditor,
+            this.selectionMoveMove,
         )
     }
 

diff --git a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
@@ -43,6 +43,7 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource {
         readonly abbreviationProvider: AbbreviationProvider,
         private readonly outputChannel: OutputChannel,
         private readonly textEditor: TextEditor,
+        private selectionMoveMoveOverride?: SelectionMoveMode,
     ) {
         this.rewriter = new AbbreviationRewriter(config, abbreviationProvider, this)
 
@@ -89,7 +90,12 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource {
     }
 
     selectionMoveMode(): SelectionMoveMode {
-        return { kind: 'OnlyMoveCursorSelections', updateUnchangedSelections: this.isVimExtensionInstalled }
+        return (
+            this.selectionMoveMoveOverride ?? {
+                kind: 'OnlyMoveCursorSelections',
+                updateUnchangedSelections: this.isVimExtensionInstalled,
+            }
+        )
     }
 
     collectSelections(): Range[] {