Skip to content

Commit ab7d4cf

Browse files
committed
multiple editors demo
1 parent bc6f8d3 commit ab7d4cf

File tree

5 files changed

+40
-22
lines changed

5 files changed

+40
-22
lines changed

Diff for: demo/src/App.css

+6-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,9 @@
11
.codeview, .infoview {
22
width: 400px;
33
height: 300px;
4-
}
4+
}
5+
6+
.controls {
7+
flex: 0 0 100%;
8+
}
9+

Diff for: demo/src/App.tsx

+26-17
Original file line numberDiff line numberDiff line change
@@ -5,26 +5,35 @@ import { LeanMonacoOptions } from 'lean4monaco'
55

66
function App() {
77
const [options, setOptions] = useState<LeanMonacoOptions>({websocket: {url: 'ws://localhost:8080/'}, vscode: {"workbench.colorTheme": "Visual Studio Light"}})
8+
const [numberEditors, setNumberEditors] = useState(1)
89

910
return (
1011
<>
11-
<button
12-
onClick={() => {setOptions({...options, vscode: {...options.vscode, "workbench.colorTheme": "Visual Studio Light"}})}}
13-
data-cy="theme-light"
14-
>Light</button>
15-
<button
16-
onClick={() => {setOptions({...options, vscode: {...options.vscode, "workbench.colorTheme": "Visual Studio Dark"}})}}
17-
data-cy="theme-dark"
18-
>Dark</button>
19-
<button
20-
onClick={() => {setOptions({...options, vscode: {...options.vscode, "lean4.input.leader": "\\"}})}}
21-
data-cy="leader-backslash"
22-
>Input Leader "\"</button>
23-
<button
24-
onClick={() => {setOptions({...options, vscode: {...options.vscode, "lean4.input.leader": ","}})}}
25-
data-cy="leader-comma"
26-
>Input Leader ","</button>
27-
<LeanMonacoComponent options={options} />
12+
<div className="controls">
13+
<button
14+
onClick={() => {setOptions({...options, vscode: {...options.vscode, "workbench.colorTheme": "Visual Studio Light"}})}}
15+
data-cy="theme-light"
16+
>Light</button>
17+
<button
18+
onClick={() => {setOptions({...options, vscode: {...options.vscode, "workbench.colorTheme": "Visual Studio Dark"}})}}
19+
data-cy="theme-dark"
20+
>Dark</button>
21+
<button
22+
onClick={() => {setOptions({...options, vscode: {...options.vscode, "lean4.input.leader": "\\"}})}}
23+
data-cy="leader-backslash"
24+
>Input Leader "\"</button>
25+
<button
26+
onClick={() => {setOptions({...options, vscode: {...options.vscode, "lean4.input.leader": ","}})}}
27+
data-cy="leader-comma"
28+
>Input Leader ","</button>
29+
<input type="number" min="1" max="3"
30+
value={numberEditors}
31+
onChange={(event) => {
32+
setNumberEditors(parseInt(event.target.value));
33+
}}
34+
/>
35+
</div>
36+
<LeanMonacoComponent options={options} numberEditors={numberEditors} />
2837
</>
2938
)
3039
}

Diff for: demo/src/LeanMonaco.tsx

+4-2
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import LeanMonacoEditorComponent from './LeanMonacoEditor';
44

55
export const LeanMonacoContext = createContext<LeanMonaco|null>(null);
66

7-
function LeanMonacoComponent({options} : {options: LeanMonacoOptions}) {
7+
function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOptions, numberEditors: number}) {
88
const [leanMonaco, setLeanMonaco] = useState<LeanMonaco|null>(null)
99
const infoviewRef = useRef<HTMLDivElement>(null)
1010

@@ -25,7 +25,9 @@ function LeanMonacoComponent({options} : {options: LeanMonacoOptions}) {
2525
return (
2626
<>
2727
<LeanMonacoContext.Provider value={leanMonaco}>
28-
<LeanMonacoEditorComponent />
28+
{[...Array(numberEditors)].map((x, i) =>
29+
<LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`}/>
30+
)}
2931
<div className='infoview' ref={infoviewRef}></div>
3032
</LeanMonacoContext.Provider>
3133
</>

Diff for: demo/src/LeanMonacoEditor.tsx

+2-2
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ import { useEffect, useRef, useContext } from 'react'
22
import { LeanMonacoEditor } from 'lean4monaco'
33
import { LeanMonacoContext } from './LeanMonaco'
44

5-
function LeanMonacoEditorComponent() {
5+
function LeanMonacoEditorComponent({fileName}: {fileName: string}) {
66
const codeviewRef = useRef<HTMLDivElement>(null)
77
const leanMonaco = useContext(LeanMonacoContext)
88

@@ -12,7 +12,7 @@ function LeanMonacoEditorComponent() {
1212

1313
;(async () => {
1414
await leanMonaco!.whenReady
15-
await leanMonacoEditor.start(codeviewRef.current!, `/project/test.lean`, '#check Nat')
15+
await leanMonacoEditor.start(codeviewRef.current!, fileName, '#check Nat')
1616
})()
1717

1818
return () => {

Diff for: demo/src/index.css

+2
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@
1616
#root {
1717
max-width: 1280px;
1818
padding: 2rem;
19+
display: flex;
20+
flex-flow: row wrap;
1921
}
2022

2123
a {

0 commit comments

Comments
 (0)