Skip to content

Commit bc6f8d3

Browse files
committed
separate editor component
1 parent 5ca3225 commit bc6f8d3

File tree

4 files changed

+43
-11
lines changed

4 files changed

+43
-11
lines changed

demo/package-lock.json

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

demo/src/LeanMonaco.tsx

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,33 @@
1-
import { useEffect, useRef } from 'react'
2-
import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
1+
import { useEffect, useRef, createContext, useState } from 'react'
2+
import { LeanMonaco, LeanMonacoOptions } from 'lean4monaco'
3+
import LeanMonacoEditorComponent from './LeanMonacoEditor';
4+
5+
export const LeanMonacoContext = createContext<LeanMonaco|null>(null);
36

47
function LeanMonacoComponent({options} : {options: LeanMonacoOptions}) {
5-
const codeviewRef = useRef<HTMLDivElement>(null)
8+
const [leanMonaco, setLeanMonaco] = useState<LeanMonaco|null>(null)
69
const infoviewRef = useRef<HTMLDivElement>(null)
710

811
useEffect(() => {
912
const leanMonaco = new LeanMonaco()
10-
const leanMonacoEditor = new LeanMonacoEditor()
13+
setLeanMonaco(leanMonaco)
14+
leanMonaco.setInfoviewElement(infoviewRef.current!)
1115

1216
;(async () => {
1317
await leanMonaco.start(options)
14-
leanMonaco.setInfoviewElement(infoviewRef.current!)
15-
await leanMonacoEditor.start(codeviewRef.current!, `/project/test.lean`, '#check Nat')
1618
})()
1719

1820
return () => {
19-
leanMonacoEditor.dispose()
2021
leanMonaco.dispose()
2122
}
2223
}, [options])
2324

2425
return (
2526
<>
26-
<div className='codeview' ref={codeviewRef}></div>
27-
<div className='infoview' ref={infoviewRef}></div>
27+
<LeanMonacoContext.Provider value={leanMonaco}>
28+
<LeanMonacoEditorComponent />
29+
<div className='infoview' ref={infoviewRef}></div>
30+
</LeanMonacoContext.Provider>
2831
</>
2932
)
3033
}

demo/src/LeanMonacoEditor.tsx

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
import { useEffect, useRef, useContext } from 'react'
2+
import { LeanMonacoEditor } from 'lean4monaco'
3+
import { LeanMonacoContext } from './LeanMonaco'
4+
5+
function LeanMonacoEditorComponent() {
6+
const codeviewRef = useRef<HTMLDivElement>(null)
7+
const leanMonaco = useContext(LeanMonacoContext)
8+
9+
useEffect(() => {
10+
if (leanMonaco) {
11+
const leanMonacoEditor = new LeanMonacoEditor()
12+
13+
;(async () => {
14+
await leanMonaco!.whenReady
15+
await leanMonacoEditor.start(codeviewRef.current!, `/project/test.lean`, '#check Nat')
16+
})()
17+
18+
return () => {
19+
leanMonacoEditor.dispose()
20+
}
21+
}
22+
}, [leanMonaco])
23+
24+
return (
25+
<div className='codeview' ref={codeviewRef}></div>
26+
)
27+
}
28+
29+
export default LeanMonacoEditorComponent

src/leanmonaco.ts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ export type LeanMonacoOptions = {
2929
}
3030

3131
export class LeanMonaco {
32-
ready: (value: void | PromiseLike<void>) => void
32+
private ready: (value: void | PromiseLike<void>) => void
3333
whenReady = new Promise<void>((resolve) => {
3434
this.ready = resolve
3535
})

0 commit comments

Comments
 (0)