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

infoview/Main.tsx

@@ -0,0 +1,134 @@
+import { PositionEvent, ConfigEvent, SyncPinEvent, TogglePinEvent, currentConfig, globalCurrentLoc,
+    ToggleAllMessagesEvent, syncPin, ServerStatus, Location, Config, defaultConfig, currentAllMessages,
+    AllMessagesEvent, PinnedLocation, locationEq} from './extension';
+import * as React from 'react';
+import { Message } from 'lean-client-js-core';
+import { Info } from './info';
+import { Messages, processMessages, ProcessedMessage } from './messages';
+import { Details } from './collapsing';
+import { useEvent } from './util';
+import { ContinueIcon, PauseIcon } from './svg_icons';
+import './tachyons.css' // stylesheet assumed by Lean widgets. See https://tachyons.io/ for documentation
+import './index.css'
+
+export const ConfigContext = React.createContext<Config>(defaultConfig);
+export const LocationContext = React.createContext<Location | null>(null);
+
+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>
+}
+
+interface InfoViewProps {
+    config?: Config;
+    messages: Message[];
+    curLoc?: Location;
+}
+
+export function InfoView(props: InfoViewProps) {
+    if (!props) { return null }
+    const {config, curLoc, messages} = props;
+    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>
+}
+
+export function Main(props: {}) {
+    const [config, setConfig] = React.useState(currentConfig);
+    useEvent(ConfigEvent, (cfg) => setConfig(cfg), []);
+
+    const [messages, setMessages] = React.useState<Message[]>(currentAllMessages);
+    useEvent(AllMessagesEvent, (msgs) => setMessages(msgs), []);
+
+    const [curLoc, setCurLoc] = React.useState<Location>(globalCurrentLoc);
+    useEvent(PositionEvent, (loc) => setCurLoc(loc), []);
+
+    return <InfoView {...{config, messages, curLoc}}/>;
+}
+
+interface InfosProps {
+    curLoc: Location;
+}
+
+function Infos(props: InfosProps): JSX.Element {
+    const {curLoc} = props;
+    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);
+        syncPin(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);
+        syncPin(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;
+}
+
+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>;
+}

infoview/server.ts → infoview/extension.ts

@@ -1,50 +1,86 @@
+/* This file contains everything that is specific to the vscode extension
+implementation of the infoview. So the idea is that lean-web-editor
+shares the rest of this infoview directory with this project. */
+
+import * as trythis from '../src/trythis';
+export {trythis};
+
+import * as c2cimg from '../media/copy-to-comment-light.svg';
+export {c2cimg};
+
+export {Location, Config, ServerStatus, PinnedLocation, defaultConfig, locationEq} from '../src/shared';
+
 import { Server, Transport, Connection, Event, TransportError, Message } from 'lean-client-js-core';
 import { ToInfoviewMessage, FromInfoviewMessage, Config, Location, defaultConfig, PinnedLocation } from '../src/shared';
+
 declare const acquireVsCodeApi;
 const vscode = acquireVsCodeApi();
 
-export function post(message: FromInfoviewMessage): void { // send a message to the extension
+function post(message: FromInfoviewMessage): void { // send a message to the extension
     vscode.postMessage(message);
 }
 
+/** Call this to instruct the editor to remove all highlighting. */
 export function clearHighlight(): void { return post({ command: 'stop_hover'}); }
+/** Call this to instruct the editor to highlight a specific piece of sourcefile. */
 export function highlightPosition(loc: Location): void { return post({ command: 'hover_position', loc}); }
+/** Call this to instruct the editor to copy the given text to a comment above the cursor. */
 export function copyToComment(text: string): void {
     post({ command: 'insert_text', text: `/-\n${text}\n-/\n`});
 }
-
+/** Call this to instruct the editor to reveal the given location. */
 export function reveal(loc: Location): void {
     post({ command: 'reveal', loc });
 }
-
+/** Call this to instruct the editor to insert the given text above the given location. */
 export function edit(loc: Location, text: string): void {
     post({ command: 'insert_text', loc, text });
 }
-
+/** Call this to instruct the editor to copy the given text to the clipboard. */
 export function copyText(text: string): void {
     post({ command: 'copy_text', text});
 }
-
+/** 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.
+ */
+export function syncPin(pins: PinnedLocation[]) {
+    post({ command: 'sync_pin', pins});
+}
+/** Fired whenever the user changes their cursor position in the source file. */
 export const PositionEvent: Event<Location> = new Event();
+/** The location as of the last firing of `PositionEvent`. */
 export let globalCurrentLoc: Location = null;
 PositionEvent.on((loc) => globalCurrentLoc = loc);
 
+/** The current config as of the last firing of `ConfigEvent`. */
 export let currentConfig: Config = defaultConfig;
+/** Triggers whenever the config is changed. */
 export const ConfigEvent: Event<Config> = new Event();
 
 ConfigEvent.on(c => {
     console.log('config updated: ', c);
 });
+/** Triggered when the user inserts text and causes pin locations to change. */
 export const SyncPinEvent: Event<{pins: PinnedLocation[]}> = new Event();
+/** Fired when the user triggers a pause command (external to the infoview). */
 export const PauseEvent: Event<unknown> = new Event();
+/** Fired when the user triggers a continue command (external to the infoview). */
 export const ContinueEvent: Event<unknown> = new Event();
+/** Fired when the user triggers a toggle updating command (external to the infoview). */
 export const ToggleUpdatingEvent: Event<unknown> = new Event();
+/** Fired when the user triggers a copy to comment command (external to the infoview). */
 export const CopyToCommentEvent: Event<unknown> = new Event();
+/** Fired when the user triggers a toggle pin command (external to the infoview). */
 export const TogglePinEvent: Event<unknown> = new Event();
+/** Fired when the lean server restarts. */
 export const ServerRestartEvent: Event<unknown> = new Event();
+/** Fired when all messages change. */
 export const AllMessagesEvent: Event<Message[]> = new Event();
+/** Fired when the user triggers a toggle all messages command (external to the infoview). */
 export const ToggleAllMessagesEvent: Event<unknown> = new Event();
-
+/** All of the messages as of the last 'AllMessagesEvent'. */
 export let currentAllMessages: Message[] = [];
 AllMessagesEvent.on((msgs) => currentAllMessages = msgs);
 ServerRestartEvent.on(() => currentAllMessages = []);
@@ -120,6 +156,7 @@ class ProxyConnectionClient implements Connection {
     }
 }
 
+/** Global instance of the lean server. */
 export const global_server = new Server(new ProxyTransport());
 global_server.logMessagesToConsole = true;
 global_server.allMessages.on(x => AllMessagesEvent.fire(x.msgs));

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,6 @@
-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 { useEvent } from './util';
-import { ContinueIcon, PauseIcon } from './svg_icons';
+import { Main } from './Main';
 
-export const ConfigContext = React.createContext<Config>(defaultConfig);
-export const LocationContext = React.createContext<Location | null>(null);
-
-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 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;
-}
-
-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>;
-}
-
-const domContainer = document.querySelector('#react_root');
+const domContainer = document.querySelector('#infoview_root');
 ReactDOM.render(<Main/>, domContainer);