Skip to content

Commit

Permalink
first RPC test
Browse files Browse the repository at this point in the history
  • Loading branch information
@joneugster
joneugster committed Mar 11, 2025
1 parent 9bd2c19 commit a4cf973
Show file tree
Hide file tree
Showing 28 changed files with 477 additions and 4,212 deletions.
79 changes: 73 additions & 6 deletions client/src/components/editor/Editor.tsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,19 @@ import { useLoadLevelQuery } from '../../state/api';
import { Markdown } from '../utils';
import * as monaco from 'monaco-editor'
import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'

import {RpcConnected, RpcConnectParams} from '@leanprover/infoview-api'
import '../../css/editor.css'
import { useSelector } from 'react-redux';
import { selectTypewriterMode } from '../../state/progress';
import { Typewriter } from './Typewriter';
import { GoalTabs } from './goal_tabs';
import { GameInfoview } from './tmp';
import { LeanClient } from 'lean4monaco/dist/vscode-lean4/vscode-lean4/src/leanclient'
// import { parseExtUri } from 'lean4monaco/dist/vscode-lean4/vscode-lean4/src/utils/exturi';

// import { LeanMonacoContext } from './LeanMonaco'
import { RpcSessionAtPos } from 'lean4monaco/dist/vscode-lean4/vscode-lean4/src/infoview'
import { Uri } from 'monaco-editor';

export function Editor() {
let { t } = useTranslation()
Expand All @@ -24,10 +30,14 @@ export function Editor() {
const editorRef = useRef<HTMLDivElement>(null)
const infoviewRef = useRef<HTMLDivElement>(null)
const gameInfoviewRef = useRef<HTMLDivElement>(null)
const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|undefined>(undefined)
const [leanMonacoEditor, setLeanMonacoEditor] = useState<LeanMonacoEditor>(undefined)
const [leanMonaco, setLeanMonaco] = useState<LeanMonaco>()
const [code, setCode] = useState<string>('')

const [client, setClient] = useState<LeanClient | null>(null)
const [uri, setUri] = useState<Uri | null>(null)
const [rpcSess, setRpcSess] = useState<RpcSessionAtPos|null>(null)

const [options, setOptions] = useState<LeanMonacoOptions>({
// placeholder. gets set below
websocket: {
Expand Down Expand Up @@ -84,9 +94,9 @@ export function Editor() {
// let infoProvider = _leanMonaco.infoProvider.editorApi

console.warn('gameId', gameId)
await leanMonacoEditor.start(editorRef.current!, `/${gameId}/${worldId}/L_${levelId}.lean`, code)
await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)

setEditor(leanMonacoEditor.editor)
setLeanMonacoEditor(leanMonacoEditor)
setLeanMonaco(_leanMonaco)

// Keeping the `code` state up-to-date with the changes in the editor
Expand All @@ -100,15 +110,72 @@ export function Editor() {
}
}, [options, infoviewRef, editorRef, gameId, worldId, levelId])

return <MonacoEditorContext.Provider value={editor}>
// RPC session: start new rpc session using `uri` and `client`
useEffect(() => {
console.log('connecting to RPC')

if (!(leanMonacoEditor?.editor) || !(leanMonaco?.clientProvider)) { return }

const updateUri = () => {
const model = leanMonacoEditor.editor.getModel()
if (model?.uri) {
setUri(model.uri)
return true
}
return false
}
const updateClient = () => {
const clients = leanMonaco.clientProvider.getClients()
if (clients?.[0]?.running) {
setClient(clients[0])
return true
}
return false
}
const tryUpdate = () => {
const uriUpdated = updateUri()
const clientUpdated = updateClient()
if (uriUpdated && clientUpdated) {
console.log('updated client and uri')
clearInterval(interval)
}
}
tryUpdate()
const interval = setInterval(tryUpdate, 500)
return () => clearInterval(interval)
}, [leanMonaco?.clientProvider, leanMonacoEditor?.editor])

// RPC session: wait until the `uri` is defined
useEffect(() => {
if (!client || !uri) { return }
console.log('connecting to RPC')
console.log(`client: ${client}`)
console.log(client)
console.log(`uri: ${uri}`)

client.sendRequest('$/lean/rpc/connect', {uri: uri.toString()} as RpcConnectParams).then(result => {
const sessionId = result.sessionId
console.debug(`session id: ${sessionId}`)
let _rpcSess = new RpcSessionAtPos(client, sessionId, uri.toString())
setRpcSess(_rpcSess)
}).catch(
reason => {console.error(`failed: ${reason}`)}
)

return () => {
rpcSess?.dispose()
}
}, [client, uri])

return <MonacoEditorContext.Provider value={{leanMonacoEditor, leanMonaco, rpcSess}}>
<div className="editor-wrapper"><Split direction='vertical' minSize={200} sizes={[50, 50]}
className={`editor-split ${typewriterMode ? 'hidden' : ''}`} >
<div ref={editorRef} id="editor" />
<div ref={infoviewRef} id="infoview" />
{/* TODO: */}
{/* <GameInfoview editorApi={null}/> */}
</Split>
{editor && typewriterMode && <Typewriter />}
{leanMonacoEditor && typewriterMode && <Typewriter />}
</div>
</MonacoEditorContext.Provider>
}
107 changes: 95 additions & 12 deletions client/src/components/editor/Typewriter.tsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import '../../css/typewriter.css'
import * as monaco from 'monaco-editor'
import { useRpcSession } from '@leanprover/infoview'
import { RpcConnectParams, useRpcSession } from '@leanprover/infoview'
import { LeanClient } from 'lean4monaco/dist/vscode-lean4/vscode-lean4/src/leanclient'
import { RpcSessionAtPos } from 'lean4monaco/dist/vscode-lean4/vscode-lean4/src/infoview'

/** The input field */
function TypewriterInput({disabled}: {disabled?: boolean}) {
Expand All @@ -21,9 +23,7 @@ function TypewriterInput({disabled}: {disabled?: boolean}) {
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)

/** Reference to the hidden multi-line editor */
const editor = React.useContext(MonacoEditorContext)

// const rpcSess = useRpcSession()
const {leanMonacoEditor, leanMonaco, rpcSess} = React.useContext(MonacoEditorContext)

/** Monaco editor requires the code to be set manually. */
function setTypewriterContent (typewriterInput: string) {
Expand All @@ -36,11 +36,94 @@ function TypewriterInput({disabled}: {disabled?: boolean}) {
if (processing) {return}
console.log('processing typewriter input')

rpcSess.client.sendRequest('$/lean/rpc/call',
{ method: "Lean.Widget.getInteractiveTermGoal",
params: {
textDocument: {
uri: rpcSess.uri.toString(),
// position: {line: 0, character: 1}
},
position: {line: 0, character: 1},
sessionId: rpcSess.sessionId
}
}
).then(result => {
console.log("Got an answer to the Rpc request!")
console.debug(result)
}).catch(reason => {
console.error(`Rpc request failed!`)
console.debug(reason)
})

rpcSess.client.sendRequest('$/lean/rpc/call',
{ method: "lean4game.test",
textDocument: {uri: rpcSess.uri},
position: {line: 0, character: 0},
sessionId: rpcSess.sessionId
}
).then(
result =>
console.log(`Got a RPC answer: ${result}`)
).catch(
reason =>
console.log(`RPC failed: ${reason}`)
)



// let uri = leanMonacoEditor?.editor?.getModel()?.uri.toString()
// let client = leanMonaco?.clientProvider?.getClients()[0]


// client.sendRequest('$/lean/rpc/connect', {uri: uri.toString()} as RpcConnectParams).then(result => {
// const sessionId = result.sessionId
// console.debug(`session id: ${sessionId}`)
// let rpcSess = new RpcSessionAtPos(client, sessionId, uri.toString())



// rpcSess.client.sendRequest('$/lean/rpc/call',
// { method: "Lean.Widget.getInteractiveTermGoal",
// params: {
// textDocument: {
// uri: rpcSess.uri.toString(),
// // position: {line: 0, character: 1}
// },
// position: {line: 0, character: 1},
// sessionId: rpcSess.sessionId
// }
// }
// ).then(result => {
// console.log("Got an answer to the Rpc request!")
// console.debug(result)
// }).catch(reason => {
// console.error(`Rpc request failed!`)
// console.debug(reason)
// })

// rpcSess.client.sendRequest('$/lean/rpc/call',
// { method: "lean4game.test",
// textDocument: {uri: rpcSess.uri},
// position: {line: 0, character: 0},
// sessionId: rpcSess.sessionId
// }
// ).then(
// result =>
// console.log(`Got a RPC answer: ${result}`)
// ).catch(
// reason =>
// console.log(`RPC failed: ${reason}`)
// )

// }).catch(
// reason => {console.error(`failed: ${reason}`)}
// )

// // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
// setDeletedChat([])

// const pos = editor.getPosition()
const pos = editor.getModel().getFullModelRange().getEndPosition()
const pos = leanMonacoEditor.editor.getModel().getFullModelRange().getEndPosition()

// rpcSess.call('Game.test', pos).then((response) => {
// console.debug('test Rpc call worked')
Expand All @@ -52,10 +135,10 @@ function TypewriterInput({disabled}: {disabled?: boolean}) {

if (typewriterInput) {
// setProcessing(true)
editor.executeEdits("typewriter", [{
leanMonacoEditor.editor.executeEdits("typewriter", [{
range: monaco.Selection.fromPositions(
pos,
editor.getModel().getFullModelRange().getEndPosition()
leanMonacoEditor.editor.getModel().getFullModelRange().getEndPosition()
),
text: typewriterInput.trim() + "\n",
forceMoveMarkers: false
Expand All @@ -65,8 +148,8 @@ function TypewriterInput({disabled}: {disabled?: boolean}) {
// loadGoals(rpcSess, uri, setProof, setCrashed)
}

editor.setPosition(pos)
}, [editor, typewriterInput])
leanMonacoEditor.editor.setPosition(pos)
}, [leanMonacoEditor.editor, typewriterInput, leanMonaco, rpcSess])

/*
Keep `typewriterInput` up-to-date with editor content and
Expand Down Expand Up @@ -168,9 +251,9 @@ export function Typewriter() {
const {gameId, worldId, levelId} = useContext(GameIdContext)
const editor = useContext(MonacoEditorContext)

const model = editor.getModel()
const uri = model.uri.toString()
const gameInfo = useGetGameInfoQuery({game: gameId})
// const model = editor.getModel()
// const uri = model.uri.toString()
// const gameInfo = useGetGameInfoQuery({game: gameId})

return <div className="typewriter">
<TypewriterInput />
Expand Down
55 changes: 0 additions & 55 deletions client/src/components/editor/infoview/collapsing.tsx
View file

This file was deleted.

53 changes: 0 additions & 53 deletions client/src/components/editor/infoview/contexts.ts
View file

This file was deleted.

Loading

0 comments on commit a4cf973

Please sign in to comment.