Skip to content

Add history navigation to typewriter input #432

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
414owen wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add history navigation to typewriter input #432

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 11 additions & 5 deletions client/src/app.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ import '@fontsource/roboto/700.css';

import './css/reset.css';
import './css/app.css';
import { PreferencesContext, WorldLevelIdContext} from './components/infoview/context';
import { HistoryContext, PreferencesContext, WorldLevelIdContext} from './components/infoview/context';
import { NO_HISTORY_INDEX } from './components/infoview/typewriter';
import UsePreferences from "./state/hooks/use_preferences"
import i18n from './i18n';
import { Popup } from './components/popup/popup';
Expand All @@ -24,6 +25,9 @@ function App() {

const {mobile, layout, isSavePreferences, language, isSuggestionsMobileMode, setLayout, setIsSavePreferences, setLanguage, setIsSuggestionsMobileMode} = UsePreferences()

// Typewriter history state (persists across game levels)
const [history, setHistory] = React.useState<string[]>([])

React.useEffect(() => {
i18n.changeLanguage(language)
}, [language])
Expand All @@ -33,10 +37,12 @@ function App() {
<GameIdContext.Provider value={gameId}>
<WorldLevelIdContext.Provider value={{worldId, levelId}}>
<PreferencesContext.Provider value={{mobile, layout, isSavePreferences, language, isSuggestionsMobileMode, setLayout, setIsSavePreferences, setLanguage, setIsSuggestionsMobileMode}}>
<React.Suspense>
<Outlet />
</React.Suspense>
<Popup />
<HistoryContext.Provider value={{history, setHistory}}>
<React.Suspense>
<Outlet />
</React.Suspense>
<Popup />
</HistoryContext.Provider>
</PreferencesContext.Provider>
</WorldLevelIdContext.Provider>
</GameIdContext.Provider>
Expand Down
17 changes: 17 additions & 0 deletions client/src/components/infoview/context.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import { InteractiveDiagnostic } from '@leanprover/infoview-api';
import { Diagnostic } from 'vscode-languageserver-types'
import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
import { PreferencesState } from '../../state/preferences';
import { NO_HISTORY_INDEX } from './typewriter';

export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
null as any)
Expand Down Expand Up @@ -126,20 +127,36 @@ export const DeletedChatContext = React.createContext<{
setShowHelp: () => {}
})

export const HistoryContext = React.createContext<{
history: string[],
setHistory: React.Dispatch<React.SetStateAction<string[]>>,
}>({
history: [],
setHistory: () => {},
});

export const InputModeContext = React.createContext<{
typewriterMode: boolean,
setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
typewriterInput: string,
setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
lockEditorMode: boolean,
setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
historyIndex: number,
setHistoryIndex: React.Dispatch<React.SetStateAction<number>>,
tempInput: string,
setTempInput: React.Dispatch<React.SetStateAction<string>>,
}>({
typewriterMode: true,
setTypewriterMode: () => {},
typewriterInput: "",
setTypewriterInput: () => {},
lockEditorMode: false,
setLockEditorMode: () => {},
historyIndex: NO_HISTORY_INDEX,
setHistoryIndex: () => {},
tempInput: "",
setTempInput: () => {},
});


Expand Down
51 changes: 47 additions & 4 deletions client/src/components/infoview/typewriter.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,14 @@ import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } fro
import { Diagnostic } from 'vscode-languageserver-types';
import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
import { DeletedChatContext, InputModeContext, MonacoEditorContext, PreferencesContext, ProofContext, WorldLevelIdContext } from './context'
import { DeletedChatContext, HistoryContext, InputModeContext, MonacoEditorContext, PreferencesContext, ProofContext, WorldLevelIdContext } from './context'
import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
import { GameHint, ProofState } from './rpc_api'
import { useTranslation } from 'react-i18next'

/* Constant for historyIndex, indicating navigation is not active */
export const NO_HISTORY_INDEX = -1;

export interface GameDiagnosticsParams {
uri: DocumentUri;
diagnostics: Diagnostic[];
Expand Down Expand Up @@ -89,7 +92,9 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
const [processing, setProcessing] = useState(false)

const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
// Typewriter state from consolidated context
const {history, setHistory} = React.useContext(HistoryContext);
const {typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode, historyIndex, setHistoryIndex, tempInput, setTempInput} = React.useContext(InputModeContext)

const inputRef = useRef<HTMLDivElement>()

Expand All @@ -110,6 +115,15 @@ export function Typewriter({disabled}: {disabled?: boolean}) {

const pos = editor.getPosition()
if (typewriterInput) {
// Add to history if not empty and not duplicate of last entry
const trimmed = typewriterInput.trim();
if (trimmed) {
setHistory(prev => {
const filtered = prev.filter(item => item !== trimmed)
return [...filtered, trimmed].slice(-100) // Keep last 100 commands
})
}

setProcessing(true)
editor.executeEdits("typewriter", [{
range: monaco.Selection.fromPositions(
Expand All @@ -120,6 +134,8 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
forceMoveMarkers: false
}])
setTypewriterInput('')
setHistoryIndex(NO_HISTORY_INDEX)
setTempInput('')
// Load proof after executing edits
loadGoals(rpcSess, uri, worldId, levelId, setProof, setCrashed)
}
Expand Down Expand Up @@ -253,14 +269,41 @@ export function Typewriter({disabled}: {disabled?: boolean}) {

useEffect(() => {
if (!oneLineEditor) return
// Run command when pressing enter
// Run command when pressing enter and handle history navigation
const l = oneLineEditor.onKeyUp((ev) => {
if (ev.code === "Enter" || ev.code === "NumpadEnter") {
runCommand()
} else if (ev.code === "ArrowUp") {
Copy link
Collaborator

@joneugster joneugster Jan 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would like ArrowUp and ArrowDown to be available to go through the previous proof states (as having them selected also highlights the corresponding chat messages)

Are there other keys we could use for the history?

Copy link
Collaborator

@joneugster joneugster Jan 8, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

btw, I do plan on having some keyboard shortcut list somewhere, so it's fine if it is a kind of hidden shortcut.

For example: Cmd+H for opening the history, Esc for closing it, and arrows to navigate inside the opened history.

// Navigate up in history
if (history.length > 0) {
if (historyIndex === NO_HISTORY_INDEX) {
// Save current input and go to last history item
setTempInput(typewriterInput)
setHistoryIndex(history.length - 1)
setTypewriterInput(history[history.length - 1])
} else if (historyIndex > 0) {
// Go to previous history item
setHistoryIndex(historyIndex - 1)
setTypewriterInput(history[historyIndex - 1])
}
}
} else if (ev.code === "ArrowDown") {
// Navigate down in history
if (historyIndex !== NO_HISTORY_INDEX) {
if (historyIndex < history.length - 1) {
// Go to next history item
setHistoryIndex(historyIndex + 1)
setTypewriterInput(history[historyIndex + 1])
} else {
// Return to current input
setHistoryIndex(NO_HISTORY_INDEX)
setTypewriterInput(tempInput)
}
}
}
})
return () => { l.dispose() }
}, [oneLineEditor, runCommand])
}, [oneLineEditor, runCommand, history, historyIndex, typewriterInput, tempInput])

// BUG: Causes `file closed` error
//TODO: Intention is to run once when loading, does that work?
Expand Down
7 changes: 4 additions & 3 deletions client/src/components/level.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl
import { store } from '../state/store'
import { Button } from './button'
import { Markdown } from './markdown'
import { hasInteractiveErrors } from './infoview/typewriter'
import { NO_HISTORY_INDEX, hasInteractiveErrors } from './infoview/typewriter'
import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
import { DualEditor } from './infoview/main'
Expand Down Expand Up @@ -233,9 +233,10 @@ function PlayableLevel() {
// Only for mobile layout
const [pageNumber, setPageNumber] = useState(0)

// set to true to prevent switching between typewriter and editor
const [lockEditorMode, setLockEditorMode] = useState(false)
const [typewriterInput, setTypewriterInput] = useState("")
const [tempInput, setTempInput] = useState("")
const [historyIndex, setHistoryIndex] = useState(NO_HISTORY_INDEX)
const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]

// When clicking on an inventory item, the inventory is overlayed by the item's doc.
Expand Down Expand Up @@ -396,7 +397,7 @@ function PlayableLevel() {
<div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
<DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
<SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
<InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode}}>
<InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode, historyIndex, setHistoryIndex, tempInput, setTempInput}}>
<ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
<EditorContext.Provider value={editorConnection}>
<MonacoEditorContext.Provider value={editor}>
Expand Down
Loading