From 02af07143bafe06831915bc3080fb8aed0256205 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 22 Jul 2024 15:14:00 +0200
Subject: [PATCH] feat: [lean4web] add option to change selectionMoveMove

---
 vscode-lean4/src/abbreviation/AbbreviationFeature.ts      | 6 +++---
 .../src/abbreviation/AbbreviationRewriterFeature.ts       | 7 +++++--
 .../src/abbreviation/VSCodeAbbreviationRewriter.ts        | 8 +++++++-
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/vscode-lean4/src/abbreviation/AbbreviationFeature.ts b/vscode-lean4/src/abbreviation/AbbreviationFeature.ts
index ee867d5c..35b4c533 100644
--- 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
index 748fa4a9..947b77ee 100644
--- 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
index d9b302fc..4df9ea96 100644
--- 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[] {