diff --git a/infoview/goal.tsx b/infoview/goal.tsx index bf83e68..b2007ed 100644 --- a/infoview/goal.tsx +++ b/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; diff --git a/infoview/index.tsx b/infoview/index.tsx index 007415b..96c99e2 100644 --- a/infoview/index.tsx +++ b/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(defaultConfig); -export const LocationContext = React.createContext(null); +const domContainer = document.querySelector('#infoview_root'); +const server = new VSCodeInfoServer(); -function StatusView(props: ServerStatus) { - return
- Tasks -

Running: {props.isRunning}

- - - - - - {props.tasks.map(t => - - - - - )} - -
File NamePos startPos endDesc
{t.file_name}{t.pos_line}:{t.pos_col}{t.end_pos_line}:{t.end_pos_col}{t.desc}
-
-} - -function Main(props: {}) { - if (!props) { return null } - const [config, setConfig] = React.useState(currentConfig); - const [messages, setMessages] = React.useState(currentAllMessages); - const [curLoc, setCurLoc] = React.useState(globalCurrentLoc); - useEvent(AllMessagesEvent, (msgs) => setMessages(msgs), []); - useEvent(PositionEvent, (loc) => setCurLoc(loc), []); - useEvent(ConfigEvent, (cfg) => setConfig(cfg), []); - if (!curLoc) return

Click somewhere in the Lean file to enable the info view.

; - const allMessages = processMessages(messages.filter((m) => curLoc && m.file_name === curLoc.file_name)); - return
- - -
- -
-} +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([]); - const isPinned = (loc: Location) => pinnedLocs.some((l) => locationEq(l, loc)); - const pinKey = React.useRef(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 <> -
- {pinnedLocs.map((loc) => - )} -
- - ; -} - -function usePaused(isPaused: boolean, t: T): T { - const old = React.useRef(t); - if (!isPaused) old.current = t; - return old.current; -} + const [curLoc, setCurLoc] = React.useState(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(false); - const allMessages = usePaused(isPaused, allMessages0); - const setOpenRef = React.useRef>>(); - useEvent(ToggleAllMessagesEvent, () => setOpenRef.current((t) => !t)); - return
- - All Messages ({allMessages.length}) - - { e.preventDefault(); setPaused(!isPaused)}} - title={isPaused ? 'continue updating' : 'pause updating'}> - {isPaused ? : } - - - -
-
; + return } -const domContainer = document.querySelector('#react_root'); ReactDOM.render(
, domContainer); diff --git a/infoview/info.tsx b/infoview/info.tsx index 8917b80..e96c8ff 100644 --- a/infoview/info.tsx +++ b/infoview/info.tsx @@ -1,7 +1,5 @@ -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'; @@ -9,6 +7,7 @@ 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(); const [error, setError] = React.useState(); @@ -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([]); 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(false); const isCurrentlyPaused = React.useRef(); @@ -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)'} {goalState && {e.preventDefault(); copyGoalToComment()}}>} - {isPinned && { e.preventDefault(); post({command: 'reveal', loc}); }} title="reveal file location">} - { e.preventDefault(); onPin(!isPinned)}} title={isPinned ? 'unpin' : 'pin'}>{isPinned ? : } + {isPinned && { e.preventDefault(); server.reveal(loc); }} title="reveal file location">} + {onPin && { e.preventDefault(); onPin(!isPinned)}} title={isPinned ? 'unpin' : 'pin'}>{isPinned ? : }} { e.preventDefault(); setPaused(!isPaused)}} title={isPaused ? 'continue updating' : 'pause updating'}>{isPaused ? : } { !isPaused && { e.preventDefault(); forceUpdate(); }} title="update"> } diff --git a/infoview/info_server.ts b/infoview/info_server.ts new file mode 100644 index 0000000..8f0f15f --- /dev/null +++ b/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; + /** Fired when the user triggers a continue command (external to the infoview). */ + ContinueEvent: Event; + /** Fired when the user triggers a toggle updating command (external to the infoview). */ + ToggleUpdatingEvent: Event; + /** Fired when the user triggers a copy to comment command (external to the infoview). */ + CopyToCommentEvent: Event; + /** Fired when the user triggers a toggle pin command (external to the infoview). */ + TogglePinEvent: Event; + /** Fired when the lean server restarts. */ + ServerRestartEvent: Event; + /** Fired when the user triggers a toggle all messages command (external to the infoview). */ + ToggleAllMessagesEvent: Event; + /** Triggered when messages change. */ + AllMessagesEvent: Event; + + dispose(); +} \ No newline at end of file diff --git a/infoview/main.tsx b/infoview/main.tsx new file mode 100644 index 0000000..53df82a --- /dev/null +++ b/infoview/main.tsx @@ -0,0 +1,111 @@ +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' +import { InfoServer } from './info_server'; +import { Location, Config, PinnedLocation, locationEq } from './types'; + +export const InfoServerContext = React.createContext(null); +export const ConfigContext = React.createContext(null); +export const AllMessagesContext = React.createContext([]); +export const LocationContext = React.createContext(null); + +interface InfoViewProps { + server: InfoServer; + loc?: Location; + config: Config; +} + +export function InfoView(props: InfoViewProps) { + if (!props || !props.server) { return null; } + const {server, config, loc} = props; + + const [messages, setMessages] = React.useState([]); + useEvent(server.AllMessagesEvent, (msgs) => setMessages(msgs)); + useEvent(server.ServerRestartEvent, _ => setMessages([])); + + if (!loc) return

Click somewhere in the Lean file to enable the info view.

; + const allMessages = processMessages(messages.filter((m) => loc && m.file_name === loc.file_name)); + return + +
+ +
+
+ + ; +} + +interface InfosProps { + curLoc: Location; +} + +function Infos(props: InfosProps): JSX.Element { + const { curLoc } = props; + const server = React.useContext(InfoServerContext); + useEvent(server.SyncPinEvent, (syncMsg) => setPinnedLocs(syncMsg.pins), []); + useEvent(server.TogglePinEvent, () => isPinned(curLoc) ? unpin()() : pin()); + const [pinnedLocs, setPinnedLocs] = React.useState([]); + const isPinned = (loc: Location) => pinnedLocs.some((l) => locationEq(l, loc)); + const pinKey = React.useRef(0); + const pin = () => { + if (isPinned(curLoc)) { return; } + pinKey.current += 1; + const pins = [...pinnedLocs, { ...curLoc, key: pinKey.current }]; + setPinnedLocs(pins); + server.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); + server.syncPin(pins); + } + return <> +
+ {pinnedLocs.map((loc) => + )} +
+ + ; +} + +function usePaused(isPaused: boolean, t: T): T { + const old = React.useRef(t); + if (!isPaused) old.current = t; + return old.current; +} + +function AllMessages({ allMessages: allMessages0 }: { allMessages: ProcessedMessage[] }): JSX.Element { + const config = React.useContext(ConfigContext); + const server = React.useContext(InfoServerContext); + const [isPaused, setPaused] = React.useState(false); + const allMessages = usePaused(isPaused, allMessages0); + const setOpenRef = React.useRef>>(); + useEvent(server.ToggleAllMessagesEvent, () => setOpenRef.current((t) => !t)); + return
+ + All Messages ({allMessages.length}) + + { e.preventDefault(); setPaused(!isPaused) }} + title={isPaused ? 'continue updating' : 'pause updating'}> + {isPaused ? : } + + + +
+
; +} diff --git a/infoview/messages.tsx b/infoview/messages.tsx index 183764c..8aa73f5 100644 --- a/infoview/messages.tsx +++ b/infoview/messages.tsx @@ -1,11 +1,11 @@ import { basename, escapeHtml, colorizeMessage } from './util'; -import { Message } from 'lean-client-js-node'; +import { Message } from 'lean-client-js-core'; import * as React from 'react'; -import { Location, Config } from '../src/shared'; import { CopyToCommentIcon, GoToFileIcon } from './svg_icons'; -import { copyToComment, reveal } from './server'; import { Widget } from './widget'; -import * as trythis from '../src/trythis'; +import { Location, Config} from './types'; +import { InfoServerContext } from './main'; +import * as trythis from './trythis'; function compareMessages(m1: Message, m2: Message): boolean { return m1.file_name === m2.file_name && @@ -20,23 +20,26 @@ interface MessageViewProps { } const MessageView = React.memo(({m}: MessageViewProps) => { + const server = React.useContext(InfoServerContext); const b = escapeHtml(basename(m.file_name)); const l = m.pos_line; const c = m.pos_col; const loc: Location = {file_name: m.file_name, column: c, line: l} const shouldColorize = m.severity === 'error'; let text = escapeHtml(m.text) - text = text.replace(trythis.regexGM, (_, tactic) => { - const command = encodeURI('command:_lean.pasteTacticSuggestion?' + - JSON.stringify([m, tactic])); - return `${trythis.magicWord}${tactic}` - }); + if (trythis) { + text = text.replace(trythis.regexGM, (_, tactic) => { + const command = encodeURI('command:_lean.pasteTacticSuggestion?' + + JSON.stringify([m, tactic])); + return `${trythis.magicWord}${tactic}` + }); + } text = shouldColorize ? colorizeMessage(text) : text; const title = `${b}:${l}:${c}`; return
{title} - { e.preventDefault(); reveal(loc); }} title="reveal file location"> - { m.widget ? null : {e.preventDefault(); copyToComment(m.text)}}> } + { e.preventDefault(); server.reveal(loc); }} title="reveal file location"> + { m.widget ? null : {e.preventDefault(); server.copyToComment(m.text)}}> }
diff --git a/infoview/server.ts b/infoview/server.ts deleted file mode 100644 index 7110aa4..0000000 --- a/infoview/server.ts +++ /dev/null @@ -1,128 +0,0 @@ -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 - vscode.postMessage(message); -} - -export function clearHighlight(): void { return post({ command: 'stop_hover'}); } -export function highlightPosition(loc: Location): void { return post({ command: 'hover_position', loc}); } -export function copyToComment(text: string): void { - post({ command: 'insert_text', text: `/-\n${text}\n-/\n`}); -} - -export function reveal(loc: Location): void { - post({ command: 'reveal', loc }); -} - -export function edit(loc: Location, text: string): void { - post({ command: 'insert_text', loc, text }); -} - -export function copyText(text: string): void { - post({ command: 'copy_text', text}); -} - -export const PositionEvent: Event = new Event(); -export let globalCurrentLoc: Location = null; -PositionEvent.on((loc) => globalCurrentLoc = loc); - -export let currentConfig: Config = defaultConfig; -export const ConfigEvent: Event = new Event(); - -ConfigEvent.on(c => { - console.log('config updated: ', c); -}); -export const SyncPinEvent: Event<{pins: PinnedLocation[]}> = new Event(); -export const PauseEvent: Event = new Event(); -export const ContinueEvent: Event = new Event(); -export const ToggleUpdatingEvent: Event = new Event(); -export const CopyToCommentEvent: Event = new Event(); -export const TogglePinEvent: Event = new Event(); -export const ServerRestartEvent: Event = new Event(); -export const AllMessagesEvent: Event = new Event(); -export const ToggleAllMessagesEvent: Event = new Event(); - -export let currentAllMessages: Message[] = []; -AllMessagesEvent.on((msgs) => currentAllMessages = msgs); -ServerRestartEvent.on(() => currentAllMessages = []); - -window.addEventListener('message', event => { // messages from the extension - const message = event.data as ToInfoviewMessage; // The JSON data our extension sent - switch (message.command) { - case 'position': PositionEvent.fire(message.loc); break; - case 'on_config_change': - currentConfig = { ...currentConfig, ...message.config }; - ConfigEvent.fire(currentConfig); - break; - case 'sync_pin': SyncPinEvent.fire(message); break; - case 'pause': PauseEvent.fire(message); break; - case 'continue': ContinueEvent.fire(message); break; - case 'toggle_updating': ToggleUpdatingEvent.fire(message); break; - case 'copy_to_comment': CopyToCommentEvent.fire(message); break; - case 'toggle_pin': TogglePinEvent.fire(message); break; - case 'restart': ServerRestartEvent.fire(message); break; - case 'all_messages': AllMessagesEvent.fire(message.messages); break; - case 'toggle_all_messages': ToggleAllMessagesEvent.fire({}); break; - case 'server_event': break; - case 'server_error': break; - } -}); - -class ProxyTransport implements Transport { - connect(): Connection { - return new ProxyConnectionClient(); - } - constructor() { } -} - -/** Forwards all of the messages between extension and webview. - * See also makeProxyTransport on the server. - */ -class ProxyConnectionClient implements Connection { - error: Event; - jsonMessage: Event; - alive: boolean; - messageListener: (event: MessageEvent) => void; - send(jsonMsg: any) { - post({ - command: 'server_request', - payload: JSON.stringify(jsonMsg), - }) - } - dispose() { - this.jsonMessage.dispose(); - this.error.dispose(); - this.alive = false; - window.removeEventListener('message', this.messageListener); - } - constructor() { - this.alive = true; - this.jsonMessage = new Event(); - this.error = new Event(); - this.messageListener = (event) => { // messages from the extension - const message = event.data as ToInfoviewMessage; // The JSON data our extension sent - // console.log('incoming:', message); - switch (message.command) { - case 'server_event': { - this.jsonMessage.fire(JSON.parse(message.payload)); - break; - } - case 'server_error': { - this.error.fire(JSON.parse(message.payload)); - break; - } - } - }; - window.addEventListener('message', this.messageListener); - } -} - -export const global_server = new Server(new ProxyTransport()); -global_server.logMessagesToConsole = true; -global_server.allMessages.on(x => AllMessagesEvent.fire(x.msgs)); -global_server.connect(); - -post({command:'request_config'}); \ No newline at end of file diff --git a/infoview/svg_icons.tsx b/infoview/svg_icons.tsx index ddc7e3f..f712574 100644 --- a/infoview/svg_icons.tsx +++ b/infoview/svg_icons.tsx @@ -8,7 +8,6 @@ https://github.com/microsoft/vscode-codicons/blob/master/LICENSE */ import * as React from 'react'; -import * as c2cimg from '../media/copy-to-comment-light.svg'; function Svg(props: {src: {attributes: {}; content: string}}) { const {src} = props; @@ -18,9 +17,19 @@ function Svg(props: {src: {attributes: {}; content: string}}) { } export function CopyToCommentIcon(): JSX.Element { - return + return + + + + + + + + + ; } + export function PinIcon(): JSX.Element { return } diff --git a/src/trythis.ts b/infoview/trythis.ts similarity index 100% rename from src/trythis.ts rename to infoview/trythis.ts diff --git a/infoview/tsconfig.json b/infoview/tsconfig.json index 147e889..3e4ec75 100644 --- a/infoview/tsconfig.json +++ b/infoview/tsconfig.json @@ -6,7 +6,6 @@ "jsx": "react", "typeRoots": [ "../node_modules/@types", - "../src/typings/" ], "sourceMap": true, "strict": false, @@ -19,6 +18,5 @@ }, "include": [ "./**/*", - "../src/typings/*" ] } diff --git a/infoview/types.ts b/infoview/types.ts new file mode 100644 index 0000000..a61f2d3 --- /dev/null +++ b/infoview/types.ts @@ -0,0 +1,34 @@ +export interface InfoViewTacticStateFilter { + name?: string; + regex: string; + match: boolean; + flags: string; +} + +export interface Config { + filterIndex: number; + infoViewTacticStateFilters: InfoViewTacticStateFilter[]; + infoViewAllErrorsOnLine: boolean; + infoViewAutoOpenShowGoal: boolean; +} +export const defaultConfig: Config = { + filterIndex: -1, + infoViewTacticStateFilters: [], + infoViewAllErrorsOnLine: true, + infoViewAutoOpenShowGoal: true, +} + +// [todo] this is probably already defined somewhere +export interface Location { + file_name: string; + line: number; + column: number; +} + +export interface PinnedLocation extends Location { + key: number; +} + +export function locationEq(l1: Location, l2: Location): boolean { + return l1.column === l2.column && l1.line === l2.line && l1.file_name === l2.file_name +} diff --git a/infoview/vscode_info_server.ts b/infoview/vscode_info_server.ts new file mode 100644 index 0000000..82ebb67 --- /dev/null +++ b/infoview/vscode_info_server.ts @@ -0,0 +1,115 @@ +import { FromInfoviewMessage, PinnedLocation, Location, ToInfoviewMessage, Config } from '../src/shared'; +import {Event, Connection, Transport, TransportError, Server, Message} from 'lean-client-js-core' +import { InfoServer } from './info_server'; +import { defaultConfig } from './types'; + +class ProxyTransport implements Transport { + connect(): Connection { + return new ProxyConnectionClient(this.post); + } + constructor(readonly post: (msg: FromInfoviewMessage) => void) { } +} + +/** Forwards all of the messages between extension and webview. + * See also makeProxyTransport on the server. + */ +class ProxyConnectionClient implements Connection { + error: Event; + jsonMessage: Event; + alive: boolean; + messageListener: (event: MessageEvent) => void; + send(jsonMsg: any) { + this.post({ + command: 'server_request', + payload: JSON.stringify(jsonMsg), + }) + } + dispose() { + this.jsonMessage.dispose(); + this.error.dispose(); + this.alive = false; + window.removeEventListener('message', this.messageListener); + } + constructor(readonly post: (m: FromInfoviewMessage) => void) { + this.alive = true; + this.jsonMessage = new Event(); + this.error = new Event(); + this.messageListener = (event) => { // messages from the extension + const message = event.data as ToInfoviewMessage; // The JSON data our extension sent + // console.log('incoming:', message); + switch (message.command) { + case 'server_event': { + this.jsonMessage.fire(JSON.parse(message.payload)); + break; + } + case 'server_error': { + this.error.fire(JSON.parse(message.payload)); + break; + } + } + }; + window.addEventListener('message', this.messageListener); + } +} + +declare const acquireVsCodeApi; +export class VSCodeInfoServer implements InfoServer { + vscode = acquireVsCodeApi(); + lean: Server; + currentConfig: Config = defaultConfig; + currentAllMessages: Message[] = []; + + constructor() { + this.lean = new Server(new ProxyTransport(this.post.bind(this))); + this.lean.logMessagesToConsole = true; + this.lean.allMessages.on(msgs => this.AllMessagesEvent.fire(msgs.msgs)); + this.lean.connect(); + window.addEventListener('message', event => { // messages from the extension + const message = event.data as ToInfoviewMessage; // The JSON data our extension sent + switch (message.command) { + case 'position': this.PositionEvent.fire(message.loc); break; + case 'on_config_change': + this.currentConfig = { ...this.currentConfig, ...message.config }; + this.ConfigEvent.fire(this.currentConfig); + break; + case 'sync_pin': this.SyncPinEvent.fire(message); break; + case 'pause': this.PauseEvent.fire(message); break; + case 'continue': this.ContinueEvent.fire(message); break; + case 'toggle_updating': this.ToggleUpdatingEvent.fire(message); break; + case 'copy_to_comment': this.CopyToCommentEvent.fire(message); break; + case 'toggle_pin': this.TogglePinEvent.fire(message); break; + case 'restart': this.ServerRestartEvent.fire(message); break; + case 'all_messages': this.AllMessagesEvent.fire(message.messages); break; + case 'toggle_all_messages': this.ToggleAllMessagesEvent.fire({}); break; + case 'server_event': break; + case 'server_error': break; + } + }); + this.AllMessagesEvent.on(msgs => this.currentAllMessages = msgs); + this.post({ command: 'request_config' }); + } + post(message: FromInfoviewMessage): void { this.vscode.postMessage(message); } + clearHighlight(): void { return this.post({ command: 'stop_hover' }); } + highlightPosition(loc: Location): void { return this.post({ command: 'hover_position', loc }); } + copyToComment(text: string): void { this.post({ command: 'insert_text', text: `/-\n${text}\n-/\n` }); } + reveal(loc: Location): void { this.post({ command: 'reveal', loc }); } + edit(loc: Location, text: string): void { this.post({ command: 'insert_text', loc, text }); } + copyText(text: string): void { this.post({ command: 'copy_text', text }); } + syncPin(pins: PinnedLocation[]) { this.post({ command: 'sync_pin', pins }); } + + SyncPinEvent: Event<{ pins: PinnedLocation[] }> = new Event(); + PauseEvent: Event = new Event(); + ContinueEvent: Event = new Event(); + ToggleUpdatingEvent: Event = new Event(); + CopyToCommentEvent: Event = new Event(); + TogglePinEvent: Event = new Event(); + ServerRestartEvent: Event = new Event(); + AllMessagesEvent: Event = new Event(); + ToggleAllMessagesEvent: Event = new Event(); + PositionEvent: Event = new Event(); + ConfigEvent: Event = new Event(); + + dispose() { + this.lean.dispose(); + } +} \ No newline at end of file diff --git a/infoview/widget.tsx b/infoview/widget.tsx index b688dfd..1e55ed0 100644 --- a/infoview/widget.tsx +++ b/infoview/widget.tsx @@ -2,8 +2,9 @@ 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 { WidgetComponent, WidgetHtml, WidgetElement, WidgetEventRequest, WidgetIdentifier } from 'lean-client-js-core'; +import { InfoServer } from './info_server'; +import { InfoServerContext } from './main'; function Popper(props: {children: React.ReactNode[]; popperContent: any; refEltTag: any; refEltAttrs: any}) { const { children, popperContent, refEltTag, refEltAttrs } = props; @@ -68,16 +69,16 @@ export type WidgetEffect = | {kind: 'custom'; key: string; value: string} | {kind: 'copy_text'; text: string} -function applyWidgetEffect(widget: WidgetIdentifier, file_name: string, effect: WidgetEffect) { +function applyWidgetEffect(server: InfoServer, widget: WidgetIdentifier, file_name: string, effect: WidgetEffect) { switch (effect.kind) { case 'insert_text': const loc = {file_name, line: widget.line, column: widget.column}; - edit(loc, effect.text); + server.edit(loc, effect.text); 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 'reveal_position': server.reveal({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break; + case 'highlight_position': server.highlightPosition({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break; + case 'clear_highlighting': server.clearHighlight(); break; + case 'copy_text': server.copyText(effect.text); break; case 'custom': console.log(`Custom widget effect: ${effect.key} -- ${effect.value}`); break; @@ -89,9 +90,10 @@ function applyWidgetEffect(widget: WidgetIdentifier, file_name: string, effect: export const Widget = React.memo(({ widget, fileName }: WidgetProps) => { const [html, setHtml] = React.useState(); + const server = React.useContext(InfoServerContext); React.useEffect(() => { async function loadHtml() { - setHtml((await global_server.send({ + setHtml((await server.lean.send({ command: 'get_widget', line: widget.line, column: widget.column, @@ -115,21 +117,21 @@ export const Widget = React.memo(({ widget, fileName }: WidgetProps) => { file_name: fileName, ...e, }; - const update_result = await global_server.send(message); + const update_result = await server.lean.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); + applyWidgetEffect(server, 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); + server.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.`) diff --git a/src/infoview.ts b/src/infoview.ts index 1b3e1da..2a97e69 100644 --- a/src/infoview.ts +++ b/src/infoview.ts @@ -359,7 +359,7 @@ export class InfoProvider implements Disposable { -
+
` diff --git a/src/server.ts b/src/server.ts index 180c4d2..2415a73 100644 --- a/src/server.ts +++ b/src/server.ts @@ -7,8 +7,13 @@ import { resolve } from 'path'; import * as username from 'username'; import { extensions, OutputChannel, TerminalOptions, window, workspace } from 'vscode'; import { LowPassFilter } from './util'; -import { ServerStatus } from './shared'; +export interface ServerStatus { + stopped: boolean; + isRunning: boolean; + numberOfTasks: number; + tasks: Task[]; +} const MAX_MESSAGES = 2**13; const MAX_MESSAGE_SIZE = 2**18; diff --git a/src/shared.ts b/src/shared.ts index 06235e0..b4081fe 100644 --- a/src/shared.ts +++ b/src/shared.ts @@ -1,30 +1,8 @@ /* This file contains all of the types that are common to the extension and the infoview. */ import { Message, Task } from 'lean-client-js-node'; - -// import { ServerStatus } from './server'; - -// [todo] this is probably already defined somewhere -export interface Location { - file_name: string; - line: number; - column: number; -} - -export interface PinnedLocation extends Location { - key: number; -} - -export function locationEq(l1: Location, l2: Location): boolean { - return l1.column === l2.column && l1.line === l2.line && l1.file_name === l2.file_name -} - -export interface ServerStatus { - stopped: boolean; - isRunning: boolean; - numberOfTasks: number; - tasks: Task[]; -} +import {Location, Config, PinnedLocation, InfoViewTacticStateFilter, locationEq} from '../infoview/types'; +export {Location, Config, PinnedLocation, InfoViewTacticStateFilter, locationEq} export interface InfoProps extends Location { widget?: string; // [note] vscode crashes if the widget is sent as a deeply nested json object. @@ -34,32 +12,11 @@ export interface InfoProps extends Location { base_name: string; // = basename(fileName) } -export interface InfoViewTacticStateFilter { - name?: string; - regex: string; - match: boolean; - flags: string; -} - -export interface Config { - filterIndex: number; - infoViewTacticStateFilters: InfoViewTacticStateFilter[]; - infoViewAllErrorsOnLine: boolean; - infoViewAutoOpenShowGoal: boolean; -} -export const defaultConfig: Config = { - filterIndex: -1, - infoViewTacticStateFilters: [], - infoViewAllErrorsOnLine: true, - infoViewAutoOpenShowGoal: true, -} /** The root state of the infoview */ export interface InfoViewState { cursorInfo: InfoProps; pinnedInfos: InfoProps[]; - // serverStatus: ServerStatus; - config: Config; messages: Message[]; diff --git a/src/tacticsuggestions.ts b/src/tacticsuggestions.ts index db9229b..4e508a6 100644 --- a/src/tacticsuggestions.ts +++ b/src/tacticsuggestions.ts @@ -4,7 +4,7 @@ import { CodeActionContext, CodeActionProvider, Command, commands, Position, Range, Selection, TextDocument, TextEditor, Uri, window } from 'vscode'; import { InfoProvider } from './infoview'; import { Server } from './server'; -import { regexGM, magicWord, regexM } from './trythis'; +import { regexGM, magicWord, regexM } from '../infoview/trythis'; /** Pastes suggestions provided by tactics such as `squeeze_simp` */ export class TacticSuggestions implements Disposable, CodeActionProvider { diff --git a/src/taskgutter.ts b/src/taskgutter.ts index b226745..7d862ee 100644 --- a/src/taskgutter.ts +++ b/src/taskgutter.ts @@ -1,7 +1,6 @@ import { Diagnostic, DiagnosticCollection, DiagnosticSeverity, Disposable, ExtensionContext, languages, OverviewRulerLane, Range, TextEditorDecorationType, Uri, window, workspace } from 'vscode'; -import { Server } from './server'; -import { ServerStatus } from './shared'; +import { Server, ServerStatus } from './server'; export class LeanTaskGutter implements Disposable { private decoration: TextEditorDecorationType; diff --git a/tsconfig.json b/tsconfig.json index 017022a..a7017ba 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -8,7 +8,7 @@ ], "sourceMap": true, "alwaysStrict": true, - "rootDir": "./src", + "rootDir": ".", "jsx": "preserve", "typeRoots": [ "./node_modules/@types",