From 99e4e74a29aa73dfb11549ad7e0600fbc32012da Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 14:43:22 +0100 Subject: [PATCH 1/9] Refactor all vscode code in to one file This is to maximise code reuse with the lean-web-editor project. All code that is specific to vscode is now in extension.ts. So it should only be necessary to implement this file to get the system to work in lean-web-editor. Additionally: - index.tsx has been split in to Main.tsx and index.tsx. index.tsx is vscode specific - Main has been split in to `Main` and `InfoView` components. This is to separate the stateful parts of Main. - onPin is now optional, if onPin is not provided then Info will not show the pin button - rename DOM id `react_root` to `infoview_root` --- infoview/Main.tsx | 134 +++++++++++++++++++++++++++ infoview/{server.ts => extension.ts} | 20 +++- infoview/goal.tsx | 2 +- infoview/index.tsx | 116 +---------------------- infoview/info.tsx | 21 +++-- infoview/messages.tsx | 6 +- infoview/svg_icons.tsx | 2 +- infoview/widget.tsx | 4 +- src/infoview.ts | 2 +- 9 files changed, 174 insertions(+), 133 deletions(-) create mode 100644 infoview/Main.tsx rename infoview/{server.ts => extension.ts} (89%) diff --git a/infoview/Main.tsx b/infoview/Main.tsx new file mode 100644 index 0000000..5f392fd --- /dev/null +++ b/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(defaultConfig); +export const LocationContext = React.createContext(null); + +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}
+
+} + +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

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
+ + +
+ +
+} + +export function Main(props: {}) { + const [config, setConfig] = React.useState(currentConfig); + useEvent(ConfigEvent, (cfg) => setConfig(cfg), []); + + const [messages, setMessages] = React.useState(currentAllMessages); + useEvent(AllMessagesEvent, (msgs) => setMessages(msgs), []); + + const [curLoc, setCurLoc] = React.useState(globalCurrentLoc); + useEvent(PositionEvent, (loc) => setCurLoc(loc), []); + + return ; +} + +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([]); + 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); + 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 <> +
+ {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 [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 ? : } + + + +
+
; +} diff --git a/infoview/server.ts b/infoview/extension.ts similarity index 89% rename from infoview/server.ts rename to infoview/extension.ts index 7110aa4..771392c 100644 --- a/infoview/server.ts +++ b/infoview/extension.ts @@ -1,9 +1,22 @@ +/* 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 * 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); } @@ -25,6 +38,11 @@ export function copyText(text: string): void { post({ command: 'copy_text', text}); } +export function syncPin(pins: PinnedLocation[]) { + post({ command: 'sync_pin', pins}); +} + + export const PositionEvent: Event = new Event(); export let globalCurrentLoc: Location = null; PositionEvent.on((loc) => globalCurrentLoc = loc); diff --git a/infoview/goal.tsx b/infoview/goal.tsx index bf83e68..c55ca95 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..4e500a7 100644 --- a/infoview/index.tsx +++ b/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(defaultConfig); -export const LocationContext = React.createContext(null); - -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 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; -} - -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 ? : } - - - -
-
; -} - -const domContainer = document.querySelector('#react_root'); +const domContainer = document.querySelector('#infoview_root'); ReactDOM.render(
, domContainer); diff --git a/infoview/info.tsx b/infoview/info.tsx index 8917b80..5550a13 100644 --- a/infoview/info.tsx +++ b/infoview/info.tsx @@ -1,7 +1,7 @@ -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 { global_server, ServerRestartEvent, AllMessagesEvent, currentAllMessages, CopyToCommentEvent, + copyToComment, PauseEvent, ContinueEvent, ToggleUpdatingEvent, reveal, Location } from './extension'; +import { LocationContext, ConfigContext } from './Main'; import { Widget } from './widget'; import { Goal } from './goal'; import { Messages, processMessages, ProcessedMessage, GetMessagesFor } from './messages'; @@ -43,9 +43,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 { @@ -141,7 +142,9 @@ function infoState(isPaused: boolean, loc: Location): InfoState { } export function Info(props: InfoProps): JSX.Element { - const {isCursor, isPinned, onPin} = props; + const isCursor = props.isCursor ?? true; + const isPinned = props.isPinned ?? false; + const onPin = props.onPin; const [isPaused, setPaused] = React.useState(false); const isCurrentlyPaused = React.useRef(); @@ -190,8 +193,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(); 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/messages.tsx b/infoview/messages.tsx index 183764c..b5875a9 100644 --- a/infoview/messages.tsx +++ b/infoview/messages.tsx @@ -1,11 +1,9 @@ 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 { trythis, Location, Config, reveal, copyToComment} from './extension'; function compareMessages(m1: Message, m2: Message): boolean { return m1.file_name === m2.file_name && diff --git a/infoview/svg_icons.tsx b/infoview/svg_icons.tsx index ddc7e3f..3b6f75f 100644 --- a/infoview/svg_icons.tsx +++ b/infoview/svg_icons.tsx @@ -8,7 +8,7 @@ https://github.com/microsoft/vscode-codicons/blob/master/LICENSE */ import * as React from 'react'; -import * as c2cimg from '../media/copy-to-comment-light.svg'; +import { c2cimg } from './extension'; function Svg(props: {src: {attributes: {}; content: string}}) { const {src} = props; diff --git a/infoview/widget.tsx b/infoview/widget.tsx index b688dfd..1d2b25f 100644 --- a/infoview/widget.tsx +++ b/infoview/widget.tsx @@ -2,8 +2,8 @@ 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 { edit, reveal, highlightPosition, clearHighlight, copyText, global_server } from './extension'; function Popper(props: {children: React.ReactNode[]; popperContent: any; refEltTag: any; refEltAttrs: any}) { const { children, popperContent, refEltTag, refEltAttrs } = props; 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 { -
+
` From 0fea8ece87ff7a2d043a366b395175954b2e1463 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 14:51:25 +0100 Subject: [PATCH 2/9] Restrict the exports from ../src/shared --- infoview/extension.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/infoview/extension.ts b/infoview/extension.ts index 771392c..84e5042 100644 --- a/infoview/extension.ts +++ b/infoview/extension.ts @@ -8,7 +8,7 @@ export {trythis}; import * as c2cimg from '../media/copy-to-comment-light.svg'; export {c2cimg}; -export * from '../src/shared'; +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'; From 5be03b47d3ab3abc99880a4c36a6a055ee816237 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 15:07:22 +0100 Subject: [PATCH 3/9] Add docstrings for the exported members of extension.ts --- infoview/extension.ts | 33 ++++++++++++++++++++++++++------- 1 file changed, 26 insertions(+), 7 deletions(-) diff --git a/infoview/extension.ts b/infoview/extension.ts index 84e5042..74e1f0b 100644 --- a/infoview/extension.ts +++ b/infoview/extension.ts @@ -20,49 +20,67 @@ function post(message: FromInfoviewMessage): void { // send a message to the ext 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 = 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 = 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 = new Event(); +/** Fired when the user triggers a continue command (external to the infoview). */ export const ContinueEvent: Event = new Event(); +/** Fired when the user triggers a toggle updating command (external to the infoview). */ export const ToggleUpdatingEvent: Event = new Event(); +/** Fired when the user triggers a copy to comment command (external to the infoview). */ export const CopyToCommentEvent: Event = new Event(); +/** Fired when the user triggers a toggle pin command (external to the infoview). */ export const TogglePinEvent: Event = new Event(); +/** Fired when the lean server restarts. */ export const ServerRestartEvent: Event = new Event(); +/** Fired when all messages change. */ export const AllMessagesEvent: Event = new Event(); +/** Fired when the user triggers a toggle all messages command (external to the infoview). */ export const ToggleAllMessagesEvent: Event = new Event(); - +/** All of the messages as of the last 'AllMessagesEvent'. */ export let currentAllMessages: Message[] = []; AllMessagesEvent.on((msgs) => currentAllMessages = msgs); ServerRestartEvent.on(() => currentAllMessages = []); @@ -138,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)); From db9655cf31737fcb982b477aaf9ddb0051efab6e Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 15:20:13 +0100 Subject: [PATCH 4/9] Make trythis code optional --- infoview/messages.tsx | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/infoview/messages.tsx b/infoview/messages.tsx index b5875a9..038853a 100644 --- a/infoview/messages.tsx +++ b/infoview/messages.tsx @@ -23,11 +23,13 @@ const MessageView = React.memo(({m}: MessageViewProps) => { 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
From 677b3d2e10faa3ae0463b0913212af13d99f087d Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 15:27:27 +0100 Subject: [PATCH 5/9] Make Main.tsx lower case --- infoview/{Main.tsx => main.tsx} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename infoview/{Main.tsx => main.tsx} (100%) diff --git a/infoview/Main.tsx b/infoview/main.tsx similarity index 100% rename from infoview/Main.tsx rename to infoview/main.tsx From 0c82b1aeec108d657e73e4c982ba29f5f3dd533b Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 16:44:58 +0100 Subject: [PATCH 6/9] Encapsulate extension comms in InfoServer --- infoview/extension.ts | 180 ++++++++++++++++------------------------ infoview/goal.tsx | 2 +- infoview/index.tsx | 6 +- infoview/info.tsx | 33 ++++---- infoview/info_server.ts | 52 ++++++++++++ infoview/main.tsx | 82 +++++++++--------- infoview/messages.tsx | 8 +- infoview/widget.tsx | 25 +++--- 8 files changed, 203 insertions(+), 185 deletions(-) create mode 100644 infoview/info_server.ts diff --git a/infoview/extension.ts b/infoview/extension.ts index 74e1f0b..b4c9d11 100644 --- a/infoview/extension.ts +++ b/infoview/extension.ts @@ -3,115 +3,22 @@ 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}; +export { trythis }; import * as c2cimg from '../media/copy-to-comment-light.svg'; -export {c2cimg}; - -export {Location, Config, ServerStatus, PinnedLocation, defaultConfig, locationEq} from '../src/shared'; +export { c2cimg }; 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(); - -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 = 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 = 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 = new Event(); -/** Fired when the user triggers a continue command (external to the infoview). */ -export const ContinueEvent: Event = new Event(); -/** Fired when the user triggers a toggle updating command (external to the infoview). */ -export const ToggleUpdatingEvent: Event = new Event(); -/** Fired when the user triggers a copy to comment command (external to the infoview). */ -export const CopyToCommentEvent: Event = new Event(); -/** Fired when the user triggers a toggle pin command (external to the infoview). */ -export const TogglePinEvent: Event = new Event(); -/** Fired when the lean server restarts. */ -export const ServerRestartEvent: Event = new Event(); -/** Fired when all messages change. */ -export const AllMessagesEvent: Event = new Event(); -/** Fired when the user triggers a toggle all messages command (external to the infoview). */ -export const ToggleAllMessagesEvent: Event = new Event(); -/** All of the messages as of the last 'AllMessagesEvent'. */ -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; - } -}); +import { ToInfoviewMessage, FromInfoviewMessage} from '../src/shared'; +import { InfoServer } from './info_server'; +import { Config, Location, PinnedLocation, ServerStatus, defaultConfig, locationEq } from '../src/shared'; +export { Config, Location, PinnedLocation, defaultConfig, locationEq, ServerStatus}; class ProxyTransport implements Transport { connect(): Connection { - return new ProxyConnectionClient(); + return new ProxyConnectionClient(this.post); } - constructor() { } + constructor(readonly post: (msg: FromInfoviewMessage) => void) { } } /** Forwards all of the messages between extension and webview. @@ -123,7 +30,7 @@ class ProxyConnectionClient implements Connection { alive: boolean; messageListener: (event: MessageEvent) => void; send(jsonMsg: any) { - post({ + this.post({ command: 'server_request', payload: JSON.stringify(jsonMsg), }) @@ -134,7 +41,7 @@ class ProxyConnectionClient implements Connection { this.alive = false; window.removeEventListener('message', this.messageListener); } - constructor() { + constructor(readonly post: (m: FromInfoviewMessage) => void) { this.alive = true; this.jsonMessage = new Event(); this.error = new Event(); @@ -156,10 +63,65 @@ 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)); -global_server.connect(); +declare const acquireVsCodeApi; +export class VSCodeInfoServer implements InfoServer { + vscode = acquireVsCodeApi(); + lean: Server; + currentConfig: Config = defaultConfig; + currentAllMessages: Message[] = []; + subscriptions: {dispose()}[] = [] + + constructor() { + this.lean = new Server(new ProxyTransport(this.post.bind(this))); + this.lean.logMessagesToConsole = true; + this.subscriptions.push(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.subscriptions.push(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(); -post({command:'request_config'}); \ No newline at end of file + dispose() { + for (const s of this.subscriptions) s.dispose(); + } +} \ No newline at end of file diff --git a/infoview/goal.tsx b/infoview/goal.tsx index c55ca95..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 './Main'; +import { ConfigContext } from './main'; interface GoalProps { goalState: string; diff --git a/infoview/index.tsx b/infoview/index.tsx index 4e500a7..bb3b1e3 100644 --- a/infoview/index.tsx +++ b/infoview/index.tsx @@ -1,6 +1,8 @@ import * as React from 'react'; import * as ReactDOM from 'react-dom'; -import { Main } from './Main'; +import { Main } from './main'; +import { VSCodeInfoServer } from './extension'; const domContainer = document.querySelector('#infoview_root'); -ReactDOM.render(
, domContainer); +const server = new VSCodeInfoServer(); +ReactDOM.render(
, domContainer); diff --git a/infoview/info.tsx b/infoview/info.tsx index 5550a13..1985df1 100644 --- a/infoview/info.tsx +++ b/infoview/info.tsx @@ -1,7 +1,6 @@ import * as React from 'react'; -import { global_server, ServerRestartEvent, AllMessagesEvent, currentAllMessages, CopyToCommentEvent, - copyToComment, PauseEvent, ContinueEvent, ToggleUpdatingEvent, reveal, Location } from './extension'; -import { LocationContext, ConfigContext } from './Main'; +import { Location } from './extension'; +import { LocationContext, ConfigContext, InfoServerContext } from './main'; import { Widget } from './widget'; import { Goal } from './goal'; import { Messages, processMessages, ProcessedMessage, GetMessagesFor } from './messages'; @@ -92,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(); @@ -104,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; @@ -125,23 +125,24 @@ 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 server = React.useContext(InfoServerContext); const isCursor = props.isCursor ?? true; const isPinned = props.isPinned ?? false; const onPin = props.onPin; @@ -157,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 = @@ -193,7 +194,7 @@ export function Info(props: InfoProps): JSX.Element { {isPinned && isPaused && ' (pinned and paused)'} {goalState && {e.preventDefault(); copyGoalToComment()}}>} - {isPinned && { e.preventDefault(); reveal(loc); }} title="reveal file location">} + {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..f1c0a64 --- /dev/null +++ b/infoview/info_server.ts @@ -0,0 +1,52 @@ +import { Server, Message, Event } from 'lean-client-js-core'; +import { Location, PinnedLocation, Config } from './extension'; + +/** a singleton class containing all of the information and events and triggers needed to render an infoview. */ +export interface InfoServer { + lean: Server; + 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; + /** Triggers whenever the config is changed. */ + ConfigEvent: Event; + /** Fired whenever the user changes their cursor position in the source file. */ + PositionEvent: Event; + + dispose(); +} \ No newline at end of file diff --git a/infoview/main.tsx b/infoview/main.tsx index 5f392fd..f69ee0c 100644 --- a/infoview/main.tsx +++ b/infoview/main.tsx @@ -1,6 +1,4 @@ -import { PositionEvent, ConfigEvent, SyncPinEvent, TogglePinEvent, currentConfig, globalCurrentLoc, - ToggleAllMessagesEvent, syncPin, ServerStatus, Location, Config, defaultConfig, currentAllMessages, - AllMessagesEvent, PinnedLocation, locationEq} from './extension'; +import { ServerStatus, Location, Config, defaultConfig, PinnedLocation, locationEq } from './extension'; import * as React from 'react'; import { Message } from 'lean-client-js-core'; import { Info } from './info'; @@ -10,8 +8,11 @@ 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'; -export const ConfigContext = React.createContext(defaultConfig); +export const InfoServerContext = React.createContext(null); +export const ConfigContext = React.createContext(null); +export const AllMessagesContext = React.createContext([]); export const LocationContext = React.createContext(null); function StatusView(props: ServerStatus) { @@ -34,36 +35,29 @@ function StatusView(props: ServerStatus) {
} -interface InfoViewProps { - config?: Config; - messages: Message[]; - curLoc?: Location; -} +export function Main(props: { server: InfoServer }) { + if (!props || !props.server) { return null; } + const server = props.server; + const [config, setConfig] = React.useState(defaultConfig); + useEvent(server.ConfigEvent, (cfg) => setConfig(cfg), []); + + const [messages, setMessages] = React.useState([]); + useEvent(server.AllMessagesEvent, (msgs) => setMessages(msgs)); + useEvent(server.ServerRestartEvent, _ => setMessages([])); + + const [curLoc, setCurLoc] = React.useState(null); + useEvent(server.PositionEvent, (loc) => setCurLoc(loc), []); -export function InfoView(props: InfoViewProps) { - if (!props) { return null } - const {config, curLoc, messages} = props; 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
+ return - -
+
+ +
+
-
-} - -export function Main(props: {}) { - const [config, setConfig] = React.useState(currentConfig); - useEvent(ConfigEvent, (cfg) => setConfig(cfg), []); - - const [messages, setMessages] = React.useState(currentAllMessages); - useEvent(AllMessagesEvent, (msgs) => setMessages(msgs), []); - - const [curLoc, setCurLoc] = React.useState(globalCurrentLoc); - useEvent(PositionEvent, (loc) => setCurLoc(loc), []); - - return ; + ; } interface InfosProps { @@ -71,18 +65,19 @@ interface InfosProps { } function Infos(props: InfosProps): JSX.Element { - const {curLoc} = props; - useEvent(SyncPinEvent, (syncMsg) => setPinnedLocs(syncMsg.pins), []); - useEvent(TogglePinEvent, () => isPinned(curLoc) ? unpin()() : pin()); + 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; } + if (isPinned(curLoc)) { return; } pinKey.current += 1; const pins = [...pinnedLocs, { ...curLoc, key: pinKey.current }]; setPinnedLocs(pins); - syncPin(pins); + server.syncPin(pins); } const unpin = (key?: number) => () => { if (key === undefined) { @@ -95,14 +90,14 @@ function Infos(props: InfosProps): JSX.Element { } const pins = pinnedLocs.filter((l) => l.key !== key); setPinnedLocs(pins); - syncPin(pins); + server.syncPin(pins); } return <>
{pinnedLocs.map((loc) => - )} + )}
- + ; } @@ -112,23 +107,24 @@ function usePaused(isPaused: boolean, t: T): T { return old.current; } -function AllMessages({allMessages: allMessages0}: {allMessages: ProcessedMessage[]}): JSX.Element { +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(ToggleAllMessagesEvent, () => setOpenRef.current((t) => !t)); + useEvent(server.ToggleAllMessagesEvent, () => setOpenRef.current((t) => !t)); return
All Messages ({allMessages.length}) { e.preventDefault(); setPaused(!isPaused)}} - title={isPaused ? 'continue updating' : 'pause updating'}> - {isPaused ? : } + onClick={e => { e.preventDefault(); setPaused(!isPaused) }} + title={isPaused ? 'continue updating' : 'pause updating'}> + {isPaused ? : } -
+
; } diff --git a/infoview/messages.tsx b/infoview/messages.tsx index 038853a..b1d2873 100644 --- a/infoview/messages.tsx +++ b/infoview/messages.tsx @@ -3,7 +3,8 @@ import { Message } from 'lean-client-js-core'; import * as React from 'react'; import { CopyToCommentIcon, GoToFileIcon } from './svg_icons'; import { Widget } from './widget'; -import { trythis, Location, Config, reveal, copyToComment} from './extension'; +import { trythis, Location, Config} from './extension'; +import { InfoServerContext } from './main'; function compareMessages(m1: Message, m2: Message): boolean { return m1.file_name === m2.file_name && @@ -18,6 +19,7 @@ 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} @@ -35,8 +37,8 @@ const MessageView = React.memo(({m}: MessageViewProps) => { 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/widget.tsx b/infoview/widget.tsx index 1d2b25f..4b834d6 100644 --- a/infoview/widget.tsx +++ b/infoview/widget.tsx @@ -3,7 +3,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-core'; -import { edit, reveal, highlightPosition, clearHighlight, copyText, global_server } from './extension'; +import { InfoServer } from './info_server'; +import { Server } from 'http'; +import { InfoServerContext } from './main'; function Popper(props: {children: React.ReactNode[]; popperContent: any; refEltTag: any; refEltAttrs: any}) { const { children, popperContent, refEltTag, refEltAttrs } = props; @@ -68,16 +70,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 +91,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 +118,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.`) From 6d2a555652fc9fd8a177e88738c9d9e5a7f54f30 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jul 2020 17:33:11 +0100 Subject: [PATCH 7/9] Create InfoServer It's an abstraction that tells you what the editor needs to implement to get infoviews to work. Note that config and position are not included as events, they should be passed in as props. --- infoview/extension.ts | 118 +-------------------------------- infoview/index.tsx | 19 +++++- infoview/info_server.ts | 12 ++-- infoview/main.tsx | 21 +++--- infoview/vscode_info_server.ts | 114 +++++++++++++++++++++++++++++++ infoview/widget.tsx | 1 - 6 files changed, 148 insertions(+), 137 deletions(-) create mode 100644 infoview/vscode_info_server.ts diff --git a/infoview/extension.ts b/infoview/extension.ts index b4c9d11..f19065d 100644 --- a/infoview/extension.ts +++ b/infoview/extension.ts @@ -8,120 +8,4 @@ export { trythis }; import * as c2cimg from '../media/copy-to-comment-light.svg'; export { c2cimg }; -import { Server, Transport, Connection, Event, TransportError, Message } from 'lean-client-js-core'; -import { ToInfoviewMessage, FromInfoviewMessage} from '../src/shared'; -import { InfoServer } from './info_server'; -import { Config, Location, PinnedLocation, ServerStatus, defaultConfig, locationEq } from '../src/shared'; -export { Config, Location, PinnedLocation, defaultConfig, locationEq, ServerStatus}; - -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[] = []; - subscriptions: {dispose()}[] = [] - - constructor() { - this.lean = new Server(new ProxyTransport(this.post.bind(this))); - this.lean.logMessagesToConsole = true; - this.subscriptions.push(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.subscriptions.push(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() { - for (const s of this.subscriptions) s.dispose(); - } -} \ No newline at end of file +export { Config, Location, PinnedLocation, ServerStatus, defaultConfig, locationEq } from '../src/shared'; diff --git a/infoview/index.tsx b/infoview/index.tsx index bb3b1e3..109098a 100644 --- a/infoview/index.tsx +++ b/infoview/index.tsx @@ -1,8 +1,21 @@ import * as React from 'react'; import * as ReactDOM from 'react-dom'; -import { Main } from './main'; -import { VSCodeInfoServer } from './extension'; +import { InfoView } from './main'; +import { VSCodeInfoServer } from './vscode_info_server'; +import { useEvent } from './util'; +import { defaultConfig, Location } from './extension'; const domContainer = document.querySelector('#infoview_root'); const server = new VSCodeInfoServer(); -ReactDOM.render(
, domContainer); + +function Main() { + const [config, setConfig] = React.useState(defaultConfig); + useEvent(server.ConfigEvent, (cfg) => setConfig(cfg), []); + + const [curLoc, setCurLoc] = React.useState(null); + useEvent(server.PositionEvent, (loc) => setCurLoc(loc), []); + + return +} + +ReactDOM.render(
, domContainer); diff --git a/infoview/info_server.ts b/infoview/info_server.ts index f1c0a64..715b9a1 100644 --- a/infoview/info_server.ts +++ b/infoview/info_server.ts @@ -3,8 +3,8 @@ import { Location, PinnedLocation, Config } from './extension'; /** a singleton class containing all of the information and events and triggers needed to render an infoview. */ export interface InfoServer { - lean: Server; - currentAllMessages: Message[]; + readonly lean: Server; + readonly currentAllMessages: Message[]; /** Call this to instruct the editor to remove all highlighting. */ clearHighlight(): void; @@ -43,10 +43,10 @@ export interface InfoServer { ToggleAllMessagesEvent: Event; /** Triggered when messages change. */ AllMessagesEvent: Event; - /** Triggers whenever the config is changed. */ - ConfigEvent: Event; - /** Fired whenever the user changes their cursor position in the source file. */ - PositionEvent: Event; + // /** Triggers whenever the config is changed. */ + // ConfigEvent: Event; + // /** Fired whenever the user changes their cursor position in the source file. */ + // PositionEvent: Event; dispose(); } \ No newline at end of file diff --git a/infoview/main.tsx b/infoview/main.tsx index f69ee0c..15fafaa 100644 --- a/infoview/main.tsx +++ b/infoview/main.tsx @@ -35,25 +35,26 @@ function StatusView(props: ServerStatus) {
} -export function Main(props: { server: InfoServer }) { +interface InfoViewProps { + server: InfoServer; + loc?: Location; + config: Config; +} + +export function InfoView(props: InfoViewProps) { if (!props || !props.server) { return null; } - const server = props.server; - const [config, setConfig] = React.useState(defaultConfig); - useEvent(server.ConfigEvent, (cfg) => setConfig(cfg), []); + const {server, config, loc} = props; const [messages, setMessages] = React.useState([]); useEvent(server.AllMessagesEvent, (msgs) => setMessages(msgs)); useEvent(server.ServerRestartEvent, _ => setMessages([])); - const [curLoc, setCurLoc] = React.useState(null); - useEvent(server.PositionEvent, (loc) => setCurLoc(loc), []); - - 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)); + 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
- +
diff --git a/infoview/vscode_info_server.ts b/infoview/vscode_info_server.ts new file mode 100644 index 0000000..c518359 --- /dev/null +++ b/infoview/vscode_info_server.ts @@ -0,0 +1,114 @@ +import { FromInfoviewMessage, PinnedLocation, Location, ToInfoviewMessage, Config, defaultConfig } from '../src/shared'; +import {Event, Connection, Transport, TransportError, Server, Message} from 'lean-client-js-core' +import { InfoServer } from './info_server'; + +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 4b834d6..1e55ed0 100644 --- a/infoview/widget.tsx +++ b/infoview/widget.tsx @@ -4,7 +4,6 @@ import * as ReactPopper from 'react-popper'; import './popper.css'; import { WidgetComponent, WidgetHtml, WidgetElement, WidgetEventRequest, WidgetIdentifier } from 'lean-client-js-core'; import { InfoServer } from './info_server'; -import { Server } from 'http'; import { InfoServerContext } from './main'; function Popper(props: {children: React.ReactNode[]; popperContent: any; refEltTag: any; refEltAttrs: any}) { From 9a551f66982b67a3f4a694f93e1df3c30064fc3a Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 10 Jul 2020 13:12:06 +0100 Subject: [PATCH 8/9] Remove some obsolete includes from tsconfig --- infoview/tsconfig.json | 2 -- 1 file changed, 2 deletions(-) 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/*" ] } From 8a87f849b77246f69e3b81b29c72c7e80df1b6fd Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 10 Jul 2020 14:05:01 +0100 Subject: [PATCH 9/9] Refactor - Remove extension.ts - Move types needed by lean-web-editor to types.ts - Move trythis.ts to infoview - Change rootDir of tsconfig from `./src` to `.` - Hardcode copy-to-comment svg in to infoview code. This means there is duplication but there is already duplication for the light/dark versions. Seems neater to just have all the svgs inline. Also means we can remove dependency on webpack svg loader. --- infoview/extension.ts | 11 -------- infoview/index.tsx | 2 +- infoview/info.tsx | 2 +- infoview/info_server.ts | 6 +---- infoview/main.tsx | 22 +--------------- infoview/messages.tsx | 3 ++- infoview/svg_icons.tsx | 13 ++++++++-- {src => infoview}/trythis.ts | 0 infoview/types.ts | 34 ++++++++++++++++++++++++ infoview/vscode_info_server.ts | 3 ++- src/server.ts | 7 ++++- src/shared.ts | 47 ++-------------------------------- src/tacticsuggestions.ts | 2 +- src/taskgutter.ts | 3 +-- tsconfig.json | 2 +- 15 files changed, 64 insertions(+), 93 deletions(-) delete mode 100644 infoview/extension.ts rename {src => infoview}/trythis.ts (100%) create mode 100644 infoview/types.ts diff --git a/infoview/extension.ts b/infoview/extension.ts deleted file mode 100644 index f19065d..0000000 --- a/infoview/extension.ts +++ /dev/null @@ -1,11 +0,0 @@ -/* 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 { Config, Location, PinnedLocation, ServerStatus, defaultConfig, locationEq } from '../src/shared'; diff --git a/infoview/index.tsx b/infoview/index.tsx index 109098a..96c99e2 100644 --- a/infoview/index.tsx +++ b/infoview/index.tsx @@ -3,7 +3,7 @@ import * as ReactDOM from 'react-dom'; import { InfoView } from './main'; import { VSCodeInfoServer } from './vscode_info_server'; import { useEvent } from './util'; -import { defaultConfig, Location } from './extension'; +import { defaultConfig, Location } from './types'; const domContainer = document.querySelector('#infoview_root'); const server = new VSCodeInfoServer(); diff --git a/infoview/info.tsx b/infoview/info.tsx index 1985df1..e96c8ff 100644 --- a/infoview/info.tsx +++ b/infoview/info.tsx @@ -1,5 +1,4 @@ import * as React from 'react'; -import { Location } from './extension'; import { LocationContext, ConfigContext, InfoServerContext } from './main'; import { Widget } from './widget'; import { Goal } from './goal'; @@ -8,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 { diff --git a/infoview/info_server.ts b/infoview/info_server.ts index 715b9a1..8f0f15f 100644 --- a/infoview/info_server.ts +++ b/infoview/info_server.ts @@ -1,5 +1,5 @@ import { Server, Message, Event } from 'lean-client-js-core'; -import { Location, PinnedLocation, Config } from './extension'; +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 { @@ -43,10 +43,6 @@ export interface InfoServer { ToggleAllMessagesEvent: Event; /** Triggered when messages change. */ AllMessagesEvent: Event; - // /** Triggers whenever the config is changed. */ - // ConfigEvent: Event; - // /** Fired whenever the user changes their cursor position in the source file. */ - // PositionEvent: Event; dispose(); } \ No newline at end of file diff --git a/infoview/main.tsx b/infoview/main.tsx index 15fafaa..53df82a 100644 --- a/infoview/main.tsx +++ b/infoview/main.tsx @@ -1,4 +1,3 @@ -import { ServerStatus, Location, Config, defaultConfig, PinnedLocation, locationEq } from './extension'; import * as React from 'react'; import { Message } from 'lean-client-js-core'; import { Info } from './info'; @@ -9,32 +8,13 @@ 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); -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}
-
-} - interface InfoViewProps { server: InfoServer; loc?: Location; diff --git a/infoview/messages.tsx b/infoview/messages.tsx index b1d2873..8aa73f5 100644 --- a/infoview/messages.tsx +++ b/infoview/messages.tsx @@ -3,8 +3,9 @@ import { Message } from 'lean-client-js-core'; import * as React from 'react'; import { CopyToCommentIcon, GoToFileIcon } from './svg_icons'; import { Widget } from './widget'; -import { trythis, Location, Config} from './extension'; +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 && diff --git a/infoview/svg_icons.tsx b/infoview/svg_icons.tsx index 3b6f75f..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 { c2cimg } from './extension'; 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/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 index c518359..82ebb67 100644 --- a/infoview/vscode_info_server.ts +++ b/infoview/vscode_info_server.ts @@ -1,6 +1,7 @@ -import { FromInfoviewMessage, PinnedLocation, Location, ToInfoviewMessage, Config, defaultConfig } from '../src/shared'; +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 { 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",