-
Notifications
You must be signed in to change notification settings - Fork 0
/
widget.tsx
41 lines (34 loc) · 1.35 KB
/
widget.tsx
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
import * as React from 'react';
import debounce from 'lodash.debounce';
import { RpcContext, EditorContext } from '@leanprover/infoview';
interface Params {
loc : any
data : string
code : string
codeHash : string
}
type InnerComponent =
React.ComponentType<{data : string, onDataChange : (new_data : string) => void }>
var module_cache : { [hash:string] : InnerComponent; } = {}
export default function(props : Params) {
const editorConnection = React.useContext(EditorContext)
const rs = React.useContext(RpcContext)
const [localData, setLocalData] = React.useState(props.data)
if (! module_cache.hasOwnProperty(props.codeHash)) {
console.log("Loading source")
const file = new File([props.code],
`widget_${props.codeHash}.js`, { type: 'text/javascript' })
const url = URL.createObjectURL(file)
console.log("Importing", file, url)
module_cache[props.codeHash] = React.lazy(() => import(url))
}
const reportChange = (newData : string, loc : any) =>
rs.call('updateInteractiveData', { newData, loc });
const debouncedChangeHandler = React.useMemo(() => debounce(reportChange, 300), [])
const handler = (newData : string) => {
setLocalData(newData)
debouncedChangeHandler(newData, props.loc)
}
return React.createElement(module_cache[props.codeHash],
{ data: localData, onDataChange: handler })
}