/* eslint-disable @typescript-eslint/no-unsafe-assignment */ import * as React from 'react'; import * as ReactPopper from 'react-popper'; import './popper.css'; import { WidgetComponent, WidgetHtml, WidgetElement, WidgetEventRequest, WidgetIdentifier } from 'lean-client-js-node'; import { global_server, edit, reveal, highlightPosition, clearHighlight, copyText } from './server'; import 'katex/dist/katex.min.css'; import * as Katex from 'react-katex'; /** Certain tags given by the lean widget code should be rendered as special components. * When rendering an element, this dictionary is first checked. */ const tagComponentDictionary = { 'InlineMath': Katex.InlineMath, 'BlockMath': Katex.BlockMath, } function Popper(props: {children: React.ReactNode[]; popperContent: any; refEltTag: any; refEltAttrs: any}) { const { children, popperContent, refEltTag, refEltAttrs } = props; const [referenceElement, setReferenceElement] = React.useState(null); const [popperElement, setPopperElement] = React.useState(null); const [arrowElement, setArrowElement] = React.useState(null); const { styles, attributes } = ReactPopper.usePopper(referenceElement, popperElement, { modifiers: [ { name: 'arrow', options: { element: arrowElement } }, { name: 'offset', options: { offset: [0, 8] } } ], }); const refElt = React.createElement(refEltTag, { ref: setReferenceElement, ...refEltAttrs }, children); return ( <> {refElt}
{popperContent}
); } export interface WidgetProps { widget?: WidgetIdentifier; fileName: string; } class WidgetErrorBoundary extends React.Component<{children: any},{error?: {message: string}}> { constructor(props) { super(props); this.state = { error: null }; } static getDerivedStateFromError(error) { return { error }; } componentDidCatch(error, errorInfo) { console.log(error, errorInfo); } componentWillReceiveProps(new_props) { this.setState({error: null}); } render() { if (this.state.error) { const message = this.state.error.message return

Widget rendering threw an error:

{message}
; } return this.props.children; } } /** [todo] pending adding to lean-client-js */ export type WidgetEffect = | {kind: 'insert_text', text: string, line?: number; column?: number; file_name?: string; insert_type?: 'relative' | 'absolute'} | {kind: 'reveal_position'; file_name: string; line: number; column: number} | {kind: 'highlight_position'; file_name: string; line: number; column: number} | {kind: 'clear_highlighting'} | {kind: 'custom'; key: string; value: string} | {kind: 'copy_text'; text: string} function applyWidgetEffect(widget: WidgetIdentifier, file_name: string, effect: WidgetEffect) { switch (effect.kind) { case 'insert_text': const insert_type = effect.insert_type ?? 'relative'; if (insert_type === 'relative') { const line = widget.line + (effect.line ?? 0); edit({file_name, line, column:0}, effect.text, 'relative'); } else if (insert_type === 'absolute') { edit({file_name:effect.file_name ?? file_name, line: effect.line, column: effect.column}, effect.text, 'absolute') } else { throw new Error(`unrecognised effect insert type ${insert_type}`); } break; case 'reveal_position': reveal({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break; case 'highlight_position': highlightPosition({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break; case 'clear_highlighting': clearHighlight(); break; case 'copy_text': copyText(effect.text); break; case 'custom': console.log(`Custom widget effect: ${effect.key} -- ${effect.value}`); break; default: console.error(`Unrecognised widget effect: ${effect}`); break; } } export const Widget = React.memo(({ widget, fileName }: WidgetProps) => { const [html, setHtml] = React.useState(); React.useEffect(() => { async function loadHtml() { setHtml((await global_server.send({ command: 'get_widget', line: widget.line, column: widget.column, id: widget.id, file_name: fileName, })).widget.html); } if (widget && !widget.html) { void loadHtml(); } else { setHtml(widget && widget.html); } }, [fileName, widget]); if (!widget) return null; async function post(e: any) { const message: WidgetEventRequest = { command: 'widget_event', line: widget.line, column: widget.column, id: widget.id, file_name: fileName, ...e, }; const update_result = await global_server.send(message); if (!update_result.record) { return; } const record = update_result.record; if (record.status === 'success' && record.widget) { const effects: WidgetEffect[] | undefined = (record as any).effects; if (effects) { for (const effect of effects) { applyWidgetEffect(widget, fileName, effect); } } setHtml(record.widget.html); } else if (record.status === 'edit') { // Lean < 3.17 const loc = { line: widget.line, column: widget.column, file_name: fileName }; edit(loc, record.action); setHtml(record.widget.html); } else if (record.status === 'invalid_handler') { console.warn(`No widget_event update for ${message.handler}: invalid handler.`) } else if (record.status === 'error') { console.error(`Update gave an error: ${record.message || record}`); } } return
{ html ? : null }
}, (a, b) => a.fileName === b.fileName && !!a.widget === !!b.widget && (!a.widget || a.widget === b.widget || a.widget.line === b.widget.line && a.widget.column === b.widget.column && a.widget.id === b.widget.id && a.widget.html === b.widget.html)); interface HtmlProps { html: WidgetComponent; post: (e: WidgetEventRequest) => void; } function isWidgetElement(w: WidgetHtml): w is WidgetElement { return (typeof w === 'object') && (w as any).t; } function ViewHtml(props: {html: WidgetHtml; post: (msg: any) => void}) { const {html, ...rest} = props; if (typeof html === 'string') { return html; } else if (!isWidgetElement(html)) { return ViewWidgetComponent({html, ...rest}); } else { return ViewWidgetElement({ w:html, ...rest }); } } function ViewWidgetElement(props: {w: WidgetElement; post: (msg: any) => void}) { const {w, post, ...rest} = props; const { c:children, tt:tooltip } = w; let tag = w.t; let { a:attributes, e:events } = w; if (tag === 'hr') { return
; } tag = tagComponentDictionary[tag] || tag; attributes = attributes || {}; events = events || {}; const new_attrs: any = {}; for (const k of Object.getOwnPropertyNames(attributes)) { new_attrs[k] = attributes[k]; } for (const k of Object.getOwnPropertyNames(events)) { if (['onClick', 'onMouseEnter', 'onMouseLeave'].includes(k)) { new_attrs[k] = (e) => post({ command: 'widget_event', kind: k as any, handler: events[k], args: { type: 'unit' } }); } else if (((tag === 'input' && attributes.type === 'text') || tag === 'select') && k === 'onChange') { new_attrs.onChange = (e) => post({ command: 'widget_event', kind: 'onChange', handler: events[k], args: { type: 'string', value: e.target.value } }); } else { throw new Error(`unrecognised event kind ${k} for ${tag}`); } } const vs = children.map(html => ViewHtml({html, post, ...rest})); if (tooltip) { return {vs} } else if (children.length > 0) { return React.createElement(tag, new_attrs, vs); } else { return React.createElement(tag, new_attrs); } } function ViewWidgetComponent(props: HtmlProps) { return props.html.c.map(html => ViewHtml({...props, html})) }