widget.tsx

/* 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}
            <div ref={setPopperElement} style={styles.popper} {...attributes.popper} className="tooltip">
                {popperContent}
                <div ref={setArrowElement} style={styles.arrow} className="arrow" />
            </div>
        </>
    );
}

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 <div className="ba b--red pa3">
            <h1>Widget rendering threw an error:</h1>
            {message}
        </div>;
      }
      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<WidgetComponent>();
    React.useEffect(() => {
        async function loadHtml() {
            try {
                setHtml((await global_server.send({
                    command: 'get_widget',
                    line: widget.line,
                    column: widget.column,
                    id: widget.id,
                    file_name: fileName,
                })).widget.html);
            } catch (e) {
                setHtml({c: ['' + e]})
            }
        }
        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 <div>
        <WidgetErrorBoundary>
            { html ? <ViewHtml html={html} post={post}/> : null }
        </WidgetErrorBoundary>
    </div>
}, (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 <hr/>; }
    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 <Popper popperContent={ViewHtml({ html: tooltip, post, ...rest })} refEltTag={tag} refEltAttrs={new_attrs} key={new_attrs.key}>
            {vs}
        </Popper>
    } 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}))
}