Refactor so that all vscode-specific infoview stuff is in vscode_info_server.ts

infoview/goal.tsx

@@ -1,6 +1,6 @@
 import * as React from 'react';
 import { colorizeMessage, escapeHtml } from './util';
-import { ConfigContext } from './index';
+import { ConfigContext } from './main';
 
 interface GoalProps {
     goalState: string;

infoview/index.tsx

@@ -1,118 +1,21 @@
-import { post, PositionEvent, ConfigEvent, SyncPinEvent, TogglePinEvent, AllMessagesEvent, currentAllMessages, currentConfig, globalCurrentLoc, ToggleAllMessagesEvent } from './server';
 import * as React from 'react';
 import * as ReactDOM from 'react-dom';
-import { ServerStatus, Config, defaultConfig,  Location, locationEq, PinnedLocation } from '../src/shared';
-import { Message } from 'lean-client-js-core';
-import './tachyons.css' // stylesheet assumed by Lean widgets. See https://tachyons.io/ for documentation
-import './index.css'
-import { Info } from './info';
-import { Messages, processMessages, ProcessedMessage } from './messages';
-import { Details } from './collapsing';
+import { InfoView } from './main';
+import { VSCodeInfoServer } from './vscode_info_server';
 import { useEvent } from './util';
-import { ContinueIcon, PauseIcon } from './svg_icons';
+import { defaultConfig, Location } from './types';
 
-export const ConfigContext = React.createContext<Config>(defaultConfig);
-export const LocationContext = React.createContext<Location | null>(null);
+const domContainer = document.querySelector('#infoview_root');
+const server = new VSCodeInfoServer();
 
-function StatusView(props: ServerStatus) {
-    return <Details>
-        <summary className="mv2 pointer">Tasks</summary>
-        <p>Running: {props.isRunning}</p>
-        <table> <tbody>
-            <tr key="header"><th>File Name</th>
-                <th>Pos start</th>
-                <th>Pos end</th>
-                <th>Desc</th></tr>
-            {props.tasks.map(t => <tr key={`${t.file_name}:${t.pos_col}:${t.pos_line}:${t.desc}`}>
-                <td>{t.file_name}</td>
-                <td>{t.pos_line}:{t.pos_col}</td>
-                <td>{t.end_pos_line}:{t.end_pos_col}</td>
-                <td>{t.desc}</td>
-            </tr>)}
-        </tbody>
-        </table>
-    </Details>
-}
-
-function Main(props: {}) {
-    if (!props) { return null }
-    const [config, setConfig] = React.useState(currentConfig);
-    const [messages, setMessages] = React.useState<Message[]>(currentAllMessages);
-    const [curLoc, setCurLoc] = React.useState<Location>(globalCurrentLoc);
-    useEvent(AllMessagesEvent, (msgs) => setMessages(msgs), []);
-    useEvent(PositionEvent, (loc) => setCurLoc(loc), []);
-    useEvent(ConfigEvent, (cfg) => setConfig(cfg), []);
-    if (!curLoc) return <p>Click somewhere in the Lean file to enable the info view.</p>;
-    const allMessages = processMessages(messages.filter((m) => curLoc && m.file_name === curLoc.file_name));
-    return <div className="ma1">
-        <ConfigContext.Provider value={config}>
-            <Infos curLoc={curLoc}/>
-            <div className="mv2"><AllMessages allMessages={allMessages}/></div>
-        </ConfigContext.Provider>
-    </div>
-}
+function Main() {
+    const [config, setConfig] = React.useState(defaultConfig);
+    useEvent(server.ConfigEvent, (cfg) => setConfig(cfg), []);
 
-function Infos({curLoc}: {curLoc: Location}): JSX.Element {
-    useEvent(SyncPinEvent, (syncMsg) => setPinnedLocs(syncMsg.pins), []);
-    useEvent(TogglePinEvent, () => isPinned(curLoc) ? unpin()() : pin());
-    const [pinnedLocs, setPinnedLocs] = React.useState<PinnedLocation[]>([]);
-    const isPinned = (loc: Location) => pinnedLocs.some((l) => locationEq(l, loc));
-    const pinKey = React.useRef<number>(0);
-    const pin = () => {
-        if (isPinned(curLoc)) {return; }
-        pinKey.current += 1;
-        const pins = [...pinnedLocs, { ...curLoc, key: pinKey.current }];
-        setPinnedLocs(pins);
-        post({command:'sync_pin', pins});
-    }
-    const unpin = (key?: number) => () => {
-        if (key === undefined) {
-            const pinned = pinnedLocs.find(p => locationEq(p, curLoc));
-            if (pinned) {
-                key = pinned.key;
-            } else {
-                return;
-            }
-        }
-        const pins = pinnedLocs.filter((l) => l.key !== key);
-        setPinnedLocs(pins);
-        post({command:'sync_pin', pins});
-    }
-    return <>
-        <div>
-            {pinnedLocs.map((loc) =>
-                <Info key={loc.key} loc={loc} isPinned={true} isCursor={false} onPin={unpin(loc.key)}/>)}
-        </div>
-        <Info loc={curLoc} isPinned={false} isCursor={true} onPin={pin}/>
-    </>;
-}
-
-function usePaused<T>(isPaused: boolean, t: T): T {
-    const old = React.useRef<T>(t);
-    if (!isPaused) old.current = t;
-    return old.current;
-}
+    const [curLoc, setCurLoc] = React.useState<Location>(null);
+    useEvent(server.PositionEvent, (loc) => setCurLoc(loc), []);
 
-function AllMessages({allMessages: allMessages0}: {allMessages: ProcessedMessage[]}): JSX.Element {
-    const config = React.useContext(ConfigContext);
-    const [isPaused, setPaused] = React.useState<boolean>(false);
-    const allMessages = usePaused(isPaused, allMessages0);
-    const setOpenRef = React.useRef<React.Dispatch<React.SetStateAction<boolean>>>();
-    useEvent(ToggleAllMessagesEvent, () => setOpenRef.current((t) => !t));
-    return <Details setOpenRef={setOpenRef} initiallyOpen={!config.infoViewAutoOpenShowGoal}>
-        <summary>
-            All Messages ({allMessages.length})
-            <span className="fr">
-                <a className="link pointer mh2 dim"
-                        onClick={e => { e.preventDefault(); setPaused(!isPaused)}}
-                        title={isPaused ? 'continue updating' : 'pause updating'}>
-                    {isPaused ? <ContinueIcon/> : <PauseIcon/>}
-                </a>
-            </span>
-        </summary>
-        <div className="ml1"> <Messages messages={allMessages}/> </div>
-    </Details>;
+    return <InfoView server={server} loc={curLoc} config={config}/>
 }
 
-const domContainer = document.querySelector('#react_root');
 ReactDOM.render(<Main/>, domContainer);

infoview/info.tsx

@@ -1,14 +1,13 @@
-import { Location } from '../src/shared';
 import * as React from 'react';
-import { post, CopyToCommentEvent, copyToComment, PauseEvent, ContinueEvent, ToggleUpdatingEvent, global_server, ServerRestartEvent, AllMessagesEvent, currentAllMessages } from './server';
-import { LocationContext, ConfigContext } from '.';
+import { LocationContext, ConfigContext, InfoServerContext } from './main';
 import { Widget } from './widget';
 import { Goal } from './goal';
 import { Messages, processMessages, ProcessedMessage, GetMessagesFor } from './messages';
 import { basename, useEvent } from './util';
 import { CopyToCommentIcon, PinnedIcon, PinIcon, ContinueIcon, PauseIcon, RefreshIcon, GoToFileIcon } from './svg_icons';
 import { Details } from './collapsing';
 import { Event, InfoResponse, CurrentTasksResponse, Message } from 'lean-client-js-core';
+import { Location } from './types';
 
 /** Older versions of Lean can't deal with multiple simul info requests so this just prevents that. */
 class OneAtATimeDispatcher {
@@ -43,9 +42,10 @@ const statusColTable: {[T in InfoStatus]: string} = {
 
 interface InfoProps {
     loc: Location;
-    isPinned: boolean;
-    isCursor: boolean;
-    onPin: (new_pin_state: boolean) => void;
+    isPinned?: boolean; // defaults to false
+    isCursor?: boolean; // defaults to true
+    /** If undefined then the pin icon will not appear and we assume pinning feature is disabled */
+    onPin?: (new_pin_state: boolean) => void;
 }
 
 function isLoading(ts: CurrentTasksResponse, l: Location): boolean {
@@ -91,7 +91,8 @@ interface InfoState {
 }
 
 function infoState(isPaused: boolean, loc: Location): InfoState {
-    const loading = useMappedEvent(global_server.tasks, false, (t) => isLoading(t, loc), [loc]);
+    const server = React.useContext(InfoServerContext);
+    const loading = useMappedEvent(server.lean.tasks, false, (t) => isLoading(t, loc), [loc]);
 
     const [response, setResponse] = React.useState<InfoResponse>();
     const [error, setError] = React.useState<string>();
@@ -103,7 +104,7 @@ function infoState(isPaused: boolean, loc: Location): InfoState {
             return;
         }
         try {
-            const info = await global_dispatcher.run(() => global_server.info(loc.file_name, loc.line, loc.column));
+            const info = await global_dispatcher.run(() => server.lean.info(loc.file_name, loc.line, loc.column));
             const widget = info.record && info.record.widget;
             if (widget && widget.line === undefined) {
                 widget.line = loc.line;
@@ -124,24 +125,27 @@ function infoState(isPaused: boolean, loc: Location): InfoState {
         }
     });
 
-    const tasksFinished = useMappedEvent(global_server.tasks, true, (t) => isDone(t) ? new Object() : false);
+    const tasksFinished = useMappedEvent(server.lean.tasks, true, (t) => isDone(t) ? new Object() : false);
     React.useEffect(() => triggerUpdate(), [loc, isPaused, tasksFinished]);
-    useEvent(ServerRestartEvent, triggerUpdate);
-    useEvent(global_server.error, triggerUpdate);
+    useEvent(server.ServerRestartEvent, triggerUpdate);
+    useEvent(server.lean.error, triggerUpdate);
 
     const config = React.useContext(ConfigContext);
     const [messages, setMessages] = React.useState<ProcessedMessage[]>([]);
     const updateMsgs = (msgs: Message[]) => {
         setMessages(loc ? processMessages(GetMessagesFor(msgs, loc, config)) : []);
     };
-    React.useEffect(() => updateMsgs(currentAllMessages), []);
-    useEvent(AllMessagesEvent, updateMsgs, [loc, config]);
+    React.useEffect(() => updateMsgs(server.currentAllMessages), []);
+    useEvent(server.AllMessagesEvent, updateMsgs, [loc, config]);
 
     return { loc, loading, response, error, messages, triggerUpdate };
 }
 
 export function Info(props: InfoProps): JSX.Element {
-    const {isCursor, isPinned, onPin} = props;
+    const server = React.useContext(InfoServerContext);
+    const isCursor = props.isCursor ?? true;
+    const isPinned = props.isPinned ?? false;
+    const onPin = props.onPin;
 
     const [isPaused, setPaused] = React.useState<boolean>(false);
     const isCurrentlyPaused = React.useRef<boolean>();
@@ -154,15 +158,15 @@ export function Info(props: InfoProps): JSX.Element {
 
     function copyGoalToComment() {
         const goal = info.record && info.record.state;
-        if (goal) copyToComment(goal);
+        if (goal) server.copyToComment(goal);
     }
 
     // If we are the cursor infoview, then we should subscribe to
     // some commands from the extension
-    useEvent(CopyToCommentEvent, () => isCursor && copyGoalToComment(), [isCursor, info]);
-    useEvent(PauseEvent, () => isCursor && setPaused(true), [isCursor]);
-    useEvent(ContinueEvent, () => isCursor && setPaused(false), [isCursor]);
-    useEvent(ToggleUpdatingEvent, () => isCursor && setPaused(!isCurrentlyPaused.current), [isCursor]);
+    useEvent(server.CopyToCommentEvent, () => isCursor && copyGoalToComment(), [isCursor, info]);
+    useEvent(server.PauseEvent, () => isCursor && setPaused(true), [isCursor]);
+    useEvent(server.ContinueEvent, () => isCursor && setPaused(false), [isCursor]);
+    useEvent(server.ToggleUpdatingEvent, () => isCursor && setPaused(!isCurrentlyPaused.current), [isCursor]);
 
     const [displayMode, setDisplayMode] = React.useState<'widget' | 'text'>('widget');
     const widgetModeSwitcher =
@@ -190,8 +194,8 @@ export function Info(props: InfoProps): JSX.Element {
                 {isPinned && isPaused && ' (pinned and paused)'}
                 <span className="fr">
                     {goalState && <a className="link pointer mh2 dim" title="copy state to comment" onClick={e => {e.preventDefault(); copyGoalToComment()}}><CopyToCommentIcon/></a>}
-                    {isPinned && <a className={'link pointer mh2 dim '} onClick={e => { e.preventDefault(); post({command: 'reveal', loc}); }} title="reveal file location"><GoToFileIcon/></a>}
-                    <a className="link pointer mh2 dim" onClick={e => { e.preventDefault(); onPin(!isPinned)}} title={isPinned ? 'unpin' : 'pin'}>{isPinned ? <PinnedIcon/> : <PinIcon/>}</a>
+                    {isPinned && <a className={'link pointer mh2 dim '} onClick={e => { e.preventDefault(); server.reveal(loc); }} title="reveal file location"><GoToFileIcon/></a>}
+                    {onPin && <a className="link pointer mh2 dim" onClick={e => { e.preventDefault(); onPin(!isPinned)}} title={isPinned ? 'unpin' : 'pin'}>{isPinned ? <PinnedIcon/> : <PinIcon/>}</a>}
                     <a className="link pointer mh2 dim" onClick={e => { e.preventDefault(); setPaused(!isPaused)}} title={isPaused ? 'continue updating' : 'pause updating'}>{isPaused ? <ContinueIcon/> : <PauseIcon/>}</a>
                     { !isPaused && <a className={'link pointer mh2 dim'} onClick={e => { e.preventDefault(); forceUpdate(); }} title="update"><RefreshIcon/></a> }
                 </span>

infoview/info_server.ts

@@ -0,0 +1,48 @@
+import { Server, Message, Event } from 'lean-client-js-core';
+import { Location, PinnedLocation } from './types';
+
+/** a singleton class containing all of the information and events and triggers needed to render an infoview. */
+export interface InfoServer {
+    readonly lean: Server;
+    readonly currentAllMessages: Message[];
+
+    /** Call this to instruct the editor to remove all highlighting. */
+    clearHighlight(): void;
+    /** Call this to instruct the editor to highlight a specific piece of sourcefile. */
+    highlightPosition(loc: Location): void;
+    /** Call this to instruct the editor to copy the given text to a comment above the cursor. */
+    copyToComment(text: string): void;
+    /** Call this to instruct the editor to reveal the given location. */
+    reveal(loc: Location): void;
+    /** Call this to instruct the editor to insert the given text above the given location. */
+    edit(loc: Location, text: string): void;
+    /** Call this to instruct the editor to copy the given text to the clipboard. */
+    copyText(text: string): void;
+    /** Call this to tell the editor that the pins have updated.
+     * This is needed because if the user inserts text above a pinned location,
+     * the editor needs to recalculate the position of the pin, once this is done the
+     * `SyncPinEvent` is fired with the new pin locations.
+     */
+    syncPin(pins: PinnedLocation[]): void;
+
+    /** Triggered when the user inserts text and causes pin locations to change. */
+    SyncPinEvent: Event<{pins: PinnedLocation[]}>;
+    /** Fired when the user triggers a pause command (external to the infoview). */
+    PauseEvent: Event<unknown>;
+    /** Fired when the user triggers a continue command (external to the infoview). */
+    ContinueEvent: Event<unknown>;
+    /** Fired when the user triggers a toggle updating command (external to the infoview). */
+    ToggleUpdatingEvent: Event<unknown>;
+    /** Fired when the user triggers a copy to comment command (external to the infoview). */
+    CopyToCommentEvent: Event<unknown>;
+    /** Fired when the user triggers a toggle pin command (external to the infoview). */
+    TogglePinEvent: Event<unknown>;
+    /** Fired when the lean server restarts. */
+    ServerRestartEvent: Event<unknown>;
+    /** Fired when the user triggers a toggle all messages command (external to the infoview). */
+    ToggleAllMessagesEvent: Event<unknown>;
+    /** Triggered when messages change. */
+    AllMessagesEvent: Event<Message[]>;
+
+    dispose();
+}