diff --git a/client/package.json b/client/package.json index 3fe8742d..46981586 100644 --- a/client/package.json +++ b/client/package.json @@ -25,6 +25,7 @@ "jotai-tanstack-query": "^0.11.0", "lean4monaco": "^1.1.16", "lz-string": "^1.5.0", + "monaco-vim": "^0.4.4", "react": "^19.2.0", "react-dom": "^19.2.0", "react-split": "^2.0.14", diff --git a/client/src/App.tsx b/client/src/App.tsx index 09e48dc1..a11babe5 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -42,6 +42,7 @@ export function App() { const editorWrapperRef = useRef(null) const editorRef = useRef(null) const infoviewRef = useRef(null) + const vimStatusBarRef = useRef(null) const firstItemRef = useRef(null) const [dragging, setDragging] = useState(false) @@ -354,6 +355,28 @@ export function App() { // eslint-disable-next-line react-hooks/exhaustive-deps }, [infoviewRef, editorRef, options, project, settings]) + // Attach or detach vim keybindings to the current editor instance. + useEffect(() => { + if (!editor || !settings.vimMode) return + let vimMode: { dispose(): void } | undefined + let cancelled = false + ;(async () => { + const { initVimMode, VimStatusBar } = await import('./editor/vim-status-bar') + if (cancelled) return + vimMode = initVimMode(editor, vimStatusBarRef.current, VimStatusBar) + })() + return () => { + cancelled = true + try { + vimMode?.dispose() + } catch (e) { + // The editor this vim mode was attached to may already be disposed + // (settings changes recreate the editor before `editor` state updates) + console.warn('[Lean4web] vim mode dispose failed', e) + } + } + }, [editor, settings.vimMode]) + /** Set editor content to the code loaded from the URL */ useEffect(() => { if (importedCode && model) model.setValue(importedCode) @@ -565,6 +588,10 @@ export function App() { ref={editorRef} className={`codeview${codeMirror ? ' hidden' : ''}`} /> +
injected by monaco-vim. + Strip the default browser chrome so it reads as part of the status line. */ +.vim-status-bar span { + /* monaco-vim sets an inline generic 'monospace' on the prompt wrapper */ + font-family: inherit !important; +} + +.vim-status-bar input { + font-family: inherit; + font-size: inherit; + color: inherit; + background: transparent; + border: none; + outline: none; + padding: 0; + margin: 0; } .editor-support-warning { diff --git a/client/src/editor/vim-status-bar.ts b/client/src/editor/vim-status-bar.ts new file mode 100644 index 00000000..501fc78d --- /dev/null +++ b/client/src/editor/vim-status-bar.ts @@ -0,0 +1,81 @@ +import { StatusBar, StatusBarInputOptions } from 'monaco-vim' + +export { initVimMode } from 'monaco-vim' + +const kbEventTocmKeyName: Record = { + "Escape": "Esc", + "ArrowUp": "Up", + "ArrowDown": "Down", + "ArrowLeft": "Left", + "ArrowRight": "Right", + "Control": "Ctrl", + " ": "Space" +} + +/** + * Map a native KeyboardEvent from the status bar's to the + * CodeMirror-style key name that monaco-vim's prompt handlers expect + * (e.g. "Esc", "Up", "Y", "Ctrl-C"). + * + * monaco-vim's own `keyName` implementation is written for Monaco's + * IKeyboardEvent and falls back to `e.key` verbatim for native events, so the + * handlers for the `:s///c` confirm prompt (which match "Y"/"N"/"A"/"Q"/"L") + * and the search/ex history (which match "Up"/"Down") never fire. + */ +function cmKeyName(e: KeyboardEvent): string { + let key = e.key + if (key in kbEventTocmKeyName) { + key = kbEventTocmKeyName[key] + } else if (key.length === 1) { + key = key.toUpperCase(); + } + // Same prefix order as monaco-vim's `monacoToCmKey` + if (e.altKey && key !== 'Alt') key = `Alt-${key}` + if (e.ctrlKey && key !== 'Ctrl') key = `Ctrl-${key}` + if (e.metaKey && key !== 'Meta') key = `Meta-${key}` + if (e.shiftKey && key !== 'Shift') key = `Shift-${key}` + return key +} + +/** + * Event facade handed to monaco-vim's prompt handlers: `keyName` returns the + * precomputed name for it, and `e_stop`/history navigation still reach the + * real event through the delegating methods and `target`. + */ +function toCmEvent(e: KeyboardEvent): KeyboardEvent { + return { + key: cmKeyName(e), + keyCode: 0, + altKey: false, + ctrlKey: false, + metaKey: false, + shiftKey: false, + target: e.target, + preventDefault: () => e.preventDefault(), + stopPropagation: () => e.stopPropagation(), + } as unknown as KeyboardEvent +} + +/** + * StatusBar that fixes key handling in the vim prompts (`:` command line, + * `/` search, and the `:s///c` confirm prompt). Without this, answering the + * confirm prompt does nothing and it cannot even be closed with Escape. + */ +export class VimStatusBar extends StatusBar { + setSec( + text: Node | string | null | undefined, + callback?: (value: string) => void, + options?: StatusBarInputOptions, + ) { + if (options) { + const { onKeyDown, onKeyUp } = options + options = { + ...options, + onKeyDown: + onKeyDown && ((e, value, close) => onKeyDown(toCmEvent(e), value, close)), + onKeyUp: onKeyUp && ((e, value, close) => onKeyUp(toCmEvent(e), value, close)), + } + } + return super.setSec(text, callback, options) + } +} diff --git a/client/src/monaco-vim.d.ts b/client/src/monaco-vim.d.ts new file mode 100644 index 00000000..8ed0cbe6 --- /dev/null +++ b/client/src/monaco-vim.d.ts @@ -0,0 +1,42 @@ +declare module 'monaco-vim' { + import type * as monaco from 'monaco-editor' + export interface VimModeInstance { + dispose(): void + } + export interface StatusBarInputOptions { + selectValueOnOpen?: boolean + value?: string + onKeyUp?: (event: KeyboardEvent, value: string, close: () => void) => void + onKeyDown?: ( + event: KeyboardEvent, + value: string, + close: () => void, + ) => boolean | void + onKeyInput?: (event: InputEvent, value: string, close: () => void) => void + onBlur?: (event: FocusEvent, close: () => void) => void + closeOnBlur?: boolean + closeOnEnter?: boolean + } + export class StatusBar { + constructor( + node: HTMLElement, + editor: monaco.editor.IStandaloneCodeEditor | null, + sanitizer?: ((node: Node) => Node) | null, + ) + setMode(ev: { mode: string; subMode?: string }): void + setSec( + text: Node | string | null | undefined, + callback?: (value: string) => void, + options?: StatusBarInputOptions, + ): (() => void) | undefined + toggleVisibility(toggle: boolean): void + closeInput: () => void + clear: () => void + } + export function initVimMode( + editor: monaco.editor.IStandaloneCodeEditor, + statusBarNode?: HTMLElement | null, + StatusBarClass?: typeof StatusBar, + sanitizer?: ((node: Node) => Node) | null, + ): VimModeInstance +} diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index a09bed86..cec01823 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -78,6 +78,16 @@ export function SettingsPopup({ />
+
+ { + updateSetting('vimMode', !newSettings.vimMode) + }} + checked={newSettings.vimMode} + /> + +
(s ?? '').replace(new RegExp(NBSP, 'g'), ' ') + +/** Load the editor with vim mode enabled and `foo foo foo` as content, + * and wait until the vim keybindings are attached. */ +function setupVim() { + cy.visit('/?vimMode=true#code=foo%20foo%20foo') + cy.get('.monaco-editor', { timeout: 30000 }).should('exist') + cy.contains('div.view-line', 'foo foo foo').should('exist') + cy.get('.vim-status-bar', { timeout: 30000 }).should('be.visible') + cy.wait(1500) + // Round-trip through insert mode: proves vim handles keys before we test + cy.get('.monaco-editor textarea.inputarea').type('i', { force: true }) + cy.get('.vim-status-bar').should('contain.text', '--INSERT--') + cy.get('.monaco-editor textarea.inputarea').type('{esc}', { force: true }) + cy.get('.vim-status-bar').should('contain.text', '--NORMAL--') + cy.get('.monaco-editor textarea.inputarea').type('0', { force: true }) +} + +function firstLine() { + return cy + .get('div.view-line') + .first() + .then(($el) => norm($el.text())) +} + +function openExPrompt(command: string) { + cy.get('.monaco-editor textarea.inputarea').type(':', { force: true }) + cy.get('.vim-status-bar input').should('exist').type(command, { delay: 50 }) +} + +describe('Vim mode', () => { + it('substitutes on the current line with :s', () => { + setupVim() + openExPrompt('s/foo/bar/{enter}') + firstLine().should('eq', 'bar foo foo') + }) + + it('substitutes everywhere with :%s//g', () => { + setupVim() + openExPrompt('%s/foo/bar/g{enter}') + firstLine().should('eq', 'bar bar bar') + }) + + it('supports the confirm flag :%s//gc, answering y, n and a', () => { + setupVim() + openExPrompt('%s/foo/bar/gc{enter}') + cy.get('.vim-status-bar').should('contain.text', 'replace with') + cy.get('.vim-status-bar input').type('y', { force: true }) + cy.get('.vim-status-bar input').type('n', { force: true }) + cy.get('.vim-status-bar input').type('a', { force: true }) + firstLine().should('eq', 'bar foo bar') + cy.get('.vim-status-bar').should('not.contain.text', 'replace with') + }) + + it('closes the confirm prompt with Escape', () => { + setupVim() + openExPrompt('%s/foo/bar/gc{enter}') + cy.get('.vim-status-bar').should('contain.text', 'replace with') + cy.get('.vim-status-bar input').type('{esc}', { force: true }) + cy.get('.vim-status-bar').should('not.contain.text', 'replace with') + firstLine().should('eq', 'foo foo foo') + }) + + it('replaces a single character with r', () => { + setupVim() + cy.get('.monaco-editor textarea.inputarea').type('rX', { + force: true, + delay: 100, + }) + firstLine().should('eq', 'Xoo foo foo') + }) + + it('overwrites text in replace mode (R)', () => { + setupVim() + cy.get('.monaco-editor textarea.inputarea').type('R', { force: true }) + cy.get('.vim-status-bar').should('contain.text', '--REPLACE--') + cy.get('.monaco-editor textarea.inputarea').type('xyz', { + force: true, + delay: 100, + }) + cy.get('.monaco-editor textarea.inputarea').type('{esc}', { force: true }) + firstLine().should('eq', 'xyz foo foo') + }) +}) diff --git a/doc/Usage.md b/doc/Usage.md index 5727bddf..9a2adedf 100644 --- a/doc/Usage.md +++ b/doc/Usage.md @@ -42,6 +42,8 @@ The recognised settings are: - `showGoalNames`: show goal names in Lean infoview box. default: `true` - `showExpectedType`: expected type in Lean infoview opened by default. default: `false` - `wordWrap`: wrap code in editor box. default: `true` + - `vimMode`: enable vim keybindings in the editor. default: `false` + - Non-boolean settings: - `ruler`: a `number`. If specified, the column at which to display the ruler. default: `` - `abbreviationCharacter`: lead character for unicode abbreviations. values: a character. default: `\` diff --git a/package-lock.json b/package-lock.json index b679c482..6e6edde9 100644 --- a/package-lock.json +++ b/package-lock.json @@ -53,6 +53,7 @@ "jotai-tanstack-query": "^0.11.0", "lean4monaco": "^1.1.16", "lz-string": "^1.5.0", + "monaco-vim": "^0.4.4", "react": "^19.2.0", "react-dom": "^19.2.0", "react-split": "^2.0.14", @@ -9075,6 +9076,15 @@ } } }, + "node_modules/monaco-vim": { + "version": "0.4.4", + "resolved": "https://registry.npmjs.org/monaco-vim/-/monaco-vim-0.4.4.tgz", + "integrity": "sha512-LNChAb//WEm/W+eyeHG/0+pdVEHotk2hLTN+M3sQZx5E8cAlSWSgqcxpcRuQnxDybSln7pfHF9i63HmbIQvrWw==", + "license": "MIT", + "peerDependencies": { + "monaco-editor": "*" + } + }, "node_modules/ms": { "version": "2.1.3", "resolved": "https://registry.npmjs.org/ms/-/ms-2.1.3.tgz",