Adding initial vim keybindings implementation

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",

client/src/App.tsx

@@ -42,6 +42,7 @@ export function App() {
   const editorWrapperRef = useRef<HTMLDivElement>(null)
   const editorRef = useRef<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
+  const vimStatusBarRef = useRef<HTMLDivElement>(null)
   const firstItemRef = useRef<HTMLSelectElement>(null)
 
   const [dragging, setDragging] = useState<boolean | null>(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' : ''}`}
           />
+          <div
+            ref={vimStatusBarRef}
+            className={`vim-status-bar${settings.vimMode && !codeMirror ? '' : ' hidden'}`}
+          />
         </div>
         <div
           ref={infoviewRef}

client/src/css/Editor.css

@@ -7,11 +7,48 @@
 .codeview-wrapper {
   width: 100%;
   position: relative;
+  display: flex;
+  flex-direction: column;
 }
 
 .codeview {
   height: 100%;
   width: 100%;
+  flex: 1;
+  min-height: 0;
+}
+
+/* Status bar for vim mode, filled by monaco-vim (e.g. "--NORMAL--") */
+.vim-status-bar {
+  flex: none;
+  font-family: 'Source Code Pro', monospace;
+  font-size: 0.85rem;
+  padding: 2px 8px;
+  color: var(--vscode-editor-foreground);
+  background-color: var(--vscode-editor-background);
+  border-top: 1px solid var(--vscode-editorWidget-border);
+}
+
+.vim-status-bar.hidden {
+  display: none;
+}
+
+/* The ex-command prompt (":w" etc.) is a bare <input> 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 {

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<string, string> = {
+  "Escape": "Esc",
+  "ArrowUp": "Up",
+  "ArrowDown": "Down",
+  "ArrowLeft": "Left",
+  "ArrowRight": "Right",
+  "Control": "Ctrl",
+   " ": "Space"
+}
+
+/**
+ * Map a native KeyboardEvent from the status bar's <input> 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)
+  }
+}

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
+}

client/src/settings/SettingsPopup.tsx

@@ -78,6 +78,16 @@ export function SettingsPopup({
           />
           <label htmlFor="wordWrap">Wrap code</label>
         </div>
+        <div>
+          <Switch
+            id="vimMode"
+            onChange={() => {
+              updateSetting('vimMode', !newSettings.vimMode)
+            }}
+            checked={newSettings.vimMode}
+          />
+          <label htmlFor="vimMode">Vim mode</label>
+        </div>
         <div>
           <Switch
             id="ruler"

client/src/settings/settings-types.ts

@@ -21,6 +21,8 @@ export interface Settings {
   theme: Theme
   /** Wrap code */
   wordWrap: boolean
+  /** Enable vim keybindings in the web editor. */
+  vimMode: boolean
   // internal: saved to browser storage
   saved: boolean
   // internal: written to search params
@@ -45,6 +47,7 @@ export const defaultSettings: UserSettings = {
   mobile: 'auto',
   theme: isBrowserDefaultDark() ? 'Visual Studio Dark' : 'Visual Studio Light',
   wordWrap: true,
+  vimMode: false,
 }
 
 export type Theme =

client/src/settings/settings-url-converters.ts

@@ -22,6 +22,7 @@ export function decodeSettingsFromURL(
     showExpectedType: parseBooleanSearchParam(searchParams, 'showExpectedType'),
     theme: decodeTheme(searchParams.get('theme') ?? undefined),
     wordWrap: parseBooleanSearchParam(searchParams, 'wordWrap'),
+    vimMode: parseBooleanSearchParam(searchParams, 'vimMode'),
   }
 }
 

cypress/e2e/vim.cy.ts

@@ -0,0 +1,85 @@
+const NBSP = String.fromCharCode(160)
+const norm = (s: string | null | undefined) => (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')
+  })
+})

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: `\`