Infoview overhaul

.eslintrc.js

@@ -22,7 +22,7 @@ module.exports = {
     ],
     "parser": "@typescript-eslint/parser",
     "parserOptions": {
-        "project": "tsconfig.json",
+        "project": ["./tsconfig.json", "./infoview/tsconfig.json"],
         "sourceType": "module"
     },
     "plugins": [
@@ -122,6 +122,7 @@ module.exports = {
         "no-console": "off",
         "no-debugger": "error",
         "no-empty": "off",
+        "ban-ts-ignore": "off",
         "no-eval": "error",
         "no-fallthrough": "off",
         "no-invalid-this": "off",

.github/workflows/on-push.yml

@@ -1,6 +1,6 @@
 name: vscode-lean build
 
-on: [push]
+on: [push, pull_request]
 
 jobs:
   build_job:

.gitignore

@@ -1,3 +1,5 @@
 out
 node_modules
 *.vsix
+media/index.js
+infoview/dist

.vscode/tasks.json

@@ -4,13 +4,24 @@
 	"version": "2.0.0",
 	"tasks": [
 		{
+			"label": "watch",
 			"type": "npm",
 			"script": "watch",
 			"problemMatcher": "$tsc-watch",
 			"isBackground": true,
 			"presentation": {
 				"reveal": "never"
 			},
+			"group": "build"
+		},
+		{
+			"label": "compile",
+			"type": "npm",
+			"script": "compile",
+			"problemMatcher": "$tsc",
+			"presentation": {
+				"reveal": "never"
+			},
 			"group": {
 				"kind": "build",
 				"isDefault": true

.vscodeignore

@@ -7,3 +7,4 @@ src/**
 .gitignore
 tsconfig.json
 vsc-extension-quickstart.md
+node_modules

infoview/custom.d.ts

@@ -0,0 +1,9 @@
+// to get importing svg files to not error.
+declare module '*.png' {
+    const content: any;
+    export default content;
+}
+declare module '*.svg' {
+    const attributes: any;
+    const content: string;
+}

infoview/event_model.ts

@@ -0,0 +1,200 @@
+import { Signal, SignalBuilder } from './util';
+import { Event, CurrentTasksResponse, WidgetEventHandler, WidgetEventRequest, WidgetData, GoalState, Message } from 'lean-client-js-core'
+import { global_server, ServerRestartEvent, ConfigEvent } from './server';
+import {Location, locationKey,} from '../src/shared';
+import { GetMessagesFor } from './messages';
+import * as React from 'react';
+
+function isLoading(ts: CurrentTasksResponse, l: Location) {
+    if (l === undefined) {return false; }
+    return ts.tasks.some(t => t.file_name === l.file_name && t.pos_line < l.line && l.line < t.end_pos_line);
+}
+function isDone(ts: CurrentTasksResponse) {
+    return ts.tasks.length === 0
+}
+
+/** Older versions of Lean can't deal with multiple simul info requests so this just prevents that. */
+class OneAtATimeDispatcher {
+    inflight = 0;
+    head: Promise<any> = new Promise((r) => r({}));
+    constructor () {}
+    run<T>(tb: () => Promise<T>): Promise<T> {
+        if (this.inflight === 0) {
+            this.inflight++;
+            this.head = tb().finally(() => {this.inflight--;});
+            return this.head;
+        } else {
+            this.inflight++;
+            this.head = this.head
+                .catch(() => ({}))
+                .then(() => tb().finally(() => {this.inflight--;}));
+            return this.head;
+        }
+    }
+}
+const global_dispatcher = new OneAtATimeDispatcher();
+
+
+interface WidgetEventArgs {
+    kind;
+    handler: WidgetEventHandler;
+    args;
+}
+
+export function infoEvents(sb: SignalBuilder, sinks: {onEdit}, onProps: Signal<InfoProps>): Signal<InfoState> {
+    const onForceUpdate = sb.mkEvent<any>();
+    const onWidgetEvent = sb.mkEvent<WidgetEventArgs>();
+    const state = sb.mkEvent<InfoState>();
+    const statev = sb.store(state);
+
+    const {loc: onLoc, isPaused: onPaused} = sb.unzip(onProps, ['loc', 'isPaused']);
+    sb.store(onLoc);
+    sb.store(onPaused);
+
+    const throttled_loc = sb.throttle<Location>(300, onLoc);
+    const onTasks = sb.throttle(300, global_server.tasks);
+    const onIsLoading = sb.map(({l, t}) => isLoading(t, l), sb.zip({l:throttled_loc, t:onTasks}));
+
+    const updateTrigger = sb.merge(sb.filter((x) => !onPaused.value, sb.merge(
+        ServerRestartEvent,
+        global_server.error,
+        sb.filter(x => !x, onPaused),
+        sb.onChange(onIsLoading),
+        sb.onChange(sb.map(isDone, onTasks)),
+        throttled_loc
+    )), onForceUpdate);
+
+    const onMessage = sb.map(({msgs, loc, config}) => {
+        return {messages: GetMessagesFor(msgs.msgs, loc, config)};
+    }, sb.zip({msgs: global_server.allMessages, loc: throttled_loc, config: ConfigEvent}));
+
+    const {result, isRunning} = sb.throttleTask<Location, Partial<InfoState>>(async () => {
+        const loc = onLoc.value;
+        if (!loc) {return {};}
+        try {
+                // [todo] if the location has not changed keep the widget and goal state?
+                const res: any = {widget: null, goalState: null, error: null};
+                const info = await global_dispatcher.run(() => global_server.info(loc.file_name, loc.line, loc.column));
+                const record = info.record;
+                res.goalState = record && record.state;
+                if (record && record.widget) {
+                    if (record.widget.html !== undefined) {
+                        res.widget = record.widget;
+                    } else {
+                        const { widget: newWidget } = await global_server.send({
+                            command: 'get_widget',
+                            line: record.widget.line,
+                            column: record.widget.column,
+                            id: record.widget.id,
+                            file_name: loc.file_name,
+                        });
+                        res.widget = newWidget;
+                    }
+                }
+                return res;
+            } catch (error) {
+                return {error};
+            }
+    }, updateTrigger);
+
+    const we = sb.mapTaskOrdered(async (e) => {
+        const s = statev.value;
+        if (!s) {return {}; }
+        if (!s.loc) {return {};}
+        if (!s.widget) {return {};}
+        const message: WidgetEventRequest = {
+            command: 'widget_event',
+            line: s.widget.line,
+            column: s.widget.column,
+            id: s.widget.id,
+            file_name: s.loc.file_name,
+            ...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) {
+            return {widget: record.widget};
+        } else if (record.status === 'edit') {
+            sinks.onEdit(s.loc, record.action);
+            return {widget: record.widget};
+        } 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}`);
+        }
+    }, onWidgetEvent);
+
+    const r: Signal<Partial<InfoState>> = sb.merge(
+        result,
+        sb.map<boolean, Partial<InfoState>>(l => ({isLoading:l}), sb.debounce(100, onIsLoading)),
+        sb.map<boolean, Partial<InfoState>>(l => ({isUpdating:l}), sb.debounce(100, isRunning)),
+        onProps,
+        we,
+        onMessage,
+    );
+
+    const defaultInfoProps: InfoState = {
+        isLoading: false,
+        isUpdating: false,
+        isPaused: false,
+        messages: [],
+        forceUpdate: () => onForceUpdate.fire({}),
+        handleWidgetEvent: (w) => onWidgetEvent.fire(w)
+    };
+    const z = sb.scan<InfoState,Partial<InfoState>>((acc, x) => ({...acc, ...x}), defaultInfoProps, r);
+    sb.push(z.on(x => state.fire(x)));
+    return state;
+}
+
+export interface InfoProps {
+    isPinned: boolean;
+    isCursor: boolean;
+    isPaused: boolean;
+    loc: Location;
+}
+
+export interface InfoSinks {
+    onEdit: (l: Location, text: string) => void;
+    onPin: (new_pin_state: boolean) => void;
+    setPaused: (paused: boolean) => void;
+}
+
+export interface InfoState {
+    loc?: Location;
+    isPaused: boolean;
+
+    isLoading: boolean;
+    isUpdating: boolean;
+    widget?: WidgetData;
+    goalState?: GoalState;
+    error?: {message: string};
+    messages: Message[];
+
+    forceUpdate: () => void;
+    handleWidgetEvent;
+}
+
+const defaultInfoState: InfoState = {
+    isLoading: false,
+    isUpdating: false,
+    isPaused: false,
+    messages: [],
+    forceUpdate: () => {},
+    handleWidgetEvent: () => {},
+}
+
+export function useInfo(ps: InfoProps, onEdit) {
+    const [g,s] = React.useState(defaultInfoState);
+    const pes = React.useRef<Event<InfoProps>>();
+    React.useEffect(() => {
+        const sb = new SignalBuilder();
+        pes.current = sb.mkEvent<InfoProps>();
+        sb.push(infoEvents(sb, {onEdit}, pes.current).on(s));
+        return () => sb.dispose();
+    }, []);
+    React.useEffect(() => {
+        pes.current.fire(ps);
+    }, [ps.isPaused, ps.loc && locationKey(ps.loc)]);
+    return g;
+}

infoview/goal.tsx

@@ -0,0 +1,28 @@
+import * as React from 'react';
+import { colorizeMessage, escapeHtml } from './util';
+import { ConfigContext } from './index';
+
+interface GoalProps {
+    goalState: string;
+}
+
+export function Goal(props: GoalProps): JSX.Element {
+    const config = React.useContext(ConfigContext);
+    if (!props.goalState) { return null; }
+    const reFilters = config.infoViewTacticStateFilters || [];
+    const filterIndex = config.filterIndex ?? -1;
+    let goalString = props.goalState.replace(/^(no goals)/mg, 'goals accomplished')
+    goalString = RegExp('^\\d+ goals|goals accomplished', 'mg').test(goalString) ? goalString : '1 goal\n'.concat(goalString);
+    if (!(reFilters.length === 0 || filterIndex === -1)) {
+        // this regex splits the goal state into (possibly multi-line) hypothesis and goal blocks
+        // by keeping indented lines with the most recent non-indented line
+        goalString = goalString.match(/(^(?!  ).*\n?(  .*\n?)*)/mg).map((line) => line.trim())
+            .filter((line) => {
+                const filt = reFilters[filterIndex];
+                const test = (new RegExp(filt.regex, filt.flags)).exec(line) !== null;
+                return filt.match ? test : !test;
+            }).join('\n');
+    }
+    goalString = colorizeMessage(escapeHtml(goalString));
+    return <pre className="font-code"  style={{whiteSpace: 'pre-wrap'}} dangerouslySetInnerHTML={{ __html: goalString }} />
+}

infoview/index.css

@@ -0,0 +1,87 @@
+
+/* Some styles specific to the infoview. */
+
+/* These are syntax highlights for the string goal view. */
+.goal-goals { color: #569cd6; }
+.goal-vdash { color: #569cd6; }
+.goal-case { color: #a1df90; }
+.goal-hyp { color: #ffcc00; }
+
+.vscode-light .goal-goals { color: #367cb6; }
+.vscode-light .goal-vdash { color: #367cb6; }
+.vscode-light .goal-case { color: #1f7a1f; }
+.vscode-light .goal-hyp { color: #cc7a00; }
+
+.highlight { /* Used to denote text highlighted by the pretty-print expression widget. */
+    background-color: #96ccff;
+}
+
+.vscode-dark .highlight {
+    background-color: #569cd6;
+}
+
+.error {
+    color: darkred;
+}
+
+.warning {
+    color: darkorange;
+}
+
+.information {
+    color: darkgreen;
+}
+
+.vscode-dark .error {
+    color: red;
+}
+
+.vscode-dark .warning {
+    color: orange;
+}
+
+.vscode-dark .information {
+    color: lightgreen;
+}
+
+.vscode-high-contrast .error {
+    color: lightpink;
+}
+
+.vscode-high-contrast .warning {
+    color: yellow;
+}
+
+.vscode-high-contrast .information {
+    color: lightgreen;
+}
+
+/* Headers for infoview */
+
+h1 {
+    display: block;
+    margin-bottom: 1ex;
+    margin-top: 1ex;
+    border-bottom: 1px solid;
+    padding: 0px;
+    font-weight: normal;
+    font-size: 100%;
+}
+
+.collapsible-header {
+    border-bottom-color: black;
+}
+.vscode-dark .collapsible-header {
+    border-bottom-color: lightgray;
+}
+.vscode-high-contrast .collapsible-header {
+    border-bottom-color: white;
+}
+
+@keyframes spinner {
+    to {transform: rotate(360deg);}
+}
+
+.spin {
+    animation: spinner .6s linear infinite;
+}