Force rerender of workspace when jump target changes

cognitive-engineering-lab · Aug 2, 2024 · cac4d8e · cac4d8e
1 parent 471de5b
commit cac4d8e
Show file tree

Hide file tree

Showing 9 changed files with 76 additions and 50 deletions.
diff --git a/ide/packages/common/src/communication.ts b/ide/packages/common/src/communication.ts
@@ -25,34 +25,55 @@ export interface TreeRenderParams {
 }
 
 export interface MessageSystem {
-  postData<T extends PanoptesToSystemCmds>(body: PanoptesToSystemMsg<T>): void;
+  postData<T extends PanoptesToSystemCmds>(
+    command: T,
+    body: Omit<PanoptesToSystemMsg<T>, "command">
+  ): void;
 
   requestData<T extends PanoptesToSystemCmds>(
-    body: PanoptesToSystemMsg<T>
+    command: T,
+    body: Omit<PanoptesToSystemMsg<T>, "command">
   ): Promise<SystemReturn<T>>;
 }
 
 export const vscodeMessageSystem: MessageSystem = {
-  postData<T extends PanoptesToSystemCmds>(body: PanoptesToSystemMsg<T>) {
-    return messageHandler.send(body.command, body);
+  postData<T extends PanoptesToSystemCmds>(
+    command: T,
+    body: Omit<PanoptesToSystemMsg<T>, "command">
+  ) {
+    return messageHandler.send(command, { command, ...body });
   },
 
-  requestData<T extends PanoptesToSystemCmds>(body: PanoptesToSystemMsg<T>) {
-    return messageHandler.request<SystemReturn<T>>(body.command, body);
+  requestData<T extends PanoptesToSystemCmds>(
+    command: T,
+    body: Omit<PanoptesToSystemMsg<T>, "command">
+  ): Promise<SystemReturn<T>> {
+    return messageHandler.request<SystemReturn<T>>(command, {
+      command,
+      ...body
+    });
   }
 };
 
 export function createClosedMessageSystem(bodies: BodyBundle[]): MessageSystem {
   const systemMap = _.groupBy(bodies, bundle => bundle.filename);
   return {
-    postData<T extends PanoptesToSystemCmds>(_body: PanoptesToSystemMsg<T>) {
+    postData<T extends PanoptesToSystemCmds>(
+      _command: T,
+      _body: Omit<PanoptesToSystemMsg<T>, "command">
+    ) {
       // Intentionally blank, no system to post to.
     },
 
-    requestData<T extends PanoptesToSystemCmds>(body: PanoptesToSystemMsg<T>) {
+    requestData<T extends PanoptesToSystemCmds>(
+      command: T,
+      bodyOmit: Omit<PanoptesToSystemMsg<T>, "command">
+    ) {
       return new Promise<SystemReturn<T>>((resolve, reject) => {
+        const body = { command, ...bodyOmit };
+
         if (!isPanoMsgTree(body)) {
-          return reject(new Error(`"Invalid message type" ${body.command}`));
+          return reject(new Error(`"Invalid message type" ${command}`));
         }
 
         const rangesInFile = systemMap[body.file];

diff --git a/ide/packages/common/src/func.ts b/ide/packages/common/src/func.ts
@@ -44,19 +44,17 @@ export function makeHighlightPosters(
   file: Filename
 ) {
   const addHighlight = () => {
-    messageSystem.postData({
+    messageSystem.postData("add-highlight", {
       type: "FROM_WEBVIEW",
       file,
-      command: "add-highlight",
       range
     });
   };
 
   const removeHighlight = () => {
-    messageSystem.postData({
+    messageSystem.postData("remove-highlight", {
       type: "FROM_WEBVIEW",
       file,
-      command: "remove-highlight",
       range
     });
   };

diff --git a/ide/packages/panoptes/src/App.tsx b/ide/packages/panoptes/src/App.tsx
@@ -38,7 +38,7 @@ import { PrintTyValue } from "@argus/print/lib";
 import classNames from "classnames";
 import MiniBuffer from "./MiniBuffer";
 import Workspace from "./Workspace";
-import { MiniBufferDataStore, highlightedObligation } from "./signals";
+import { HighlightTargetStore, MiniBufferDataStore } from "./signals";
 
 const webSysSpec: SystemSpec = {
   osPlatform: "web-bundle",
@@ -77,7 +77,7 @@ function listener(
   console.debug("Received message from system", payload);
 
   if (isSysMsgOpenError(payload)) {
-    return highlightedObligation.set(payload);
+    return HighlightTargetStore.set(payload);
   } else if (isSysMsgOpenFile(payload)) {
     return setOpenFiles(currFiles => {
       const newEntry = {
@@ -141,9 +141,8 @@ const mkLocationActionable =
       if (selectKeys(event)) {
         event.preventDefault();
         event.stopPropagation();
-        system.postData({
+        system.postData("jump-to-def", {
           type: "FROM_WEBVIEW",
-          command: "jump-to-def",
           location
         });
       }
@@ -240,13 +239,19 @@ const App = observer(({ config }: { config: PanoptesConfig }) => {
         () => MiniBufferDataStore.pin(),
         () => MiniBufferDataStore.unpin()
       );
+
     window.addEventListener("message", listen);
-    if (config.target !== undefined) {
-      highlightedObligation.set(config.target);
-    }
     return () => window.removeEventListener("message", listen);
   }, []);
 
+  useEffect(() => {
+    if (config.target !== undefined) {
+      HighlightTargetStore.set(config.target);
+    }
+
+    return () => HighlightTargetStore.reset();
+  }, [config.target]);
+
   const Navbar = (
     <>
       <div className="app-nav">
@@ -273,7 +278,11 @@ const App = observer(({ config }: { config: PanoptesConfig }) => {
                 <LocationActionable.Provider
                   value={mkLocationActionable(messageSystem)}
                 >
-                  <Workspace files={openFiles} reset={resetState} />
+                  <Workspace
+                    key={HighlightTargetStore.value?.hash ?? 0}
+                    files={openFiles}
+                    reset={resetState}
+                  />
                   <FillScreen />
                 </LocationActionable.Provider>
               </ProjectionPathRender.Provider>

diff --git a/ide/packages/panoptes/src/Code.css b/ide/packages/panoptes/src/Code.css
@@ -1,6 +1,6 @@
 pre.shiki {
     /* Shiki sets a background color inline, we need to override it. */
-    background-color: var(--background) !important;
+    background-color: transparent!important;
 
     /* Make the default element inline (to use as directory label) */
     display: inline;
@@ -9,15 +9,15 @@ pre.shiki {
 /* The code should always blend in with the view panel */
 
 .shiki code {
+  background-color: transparent;
   font-family: var(--vscode-editor-font-family);
-  background-color: var(--background);
 }
 
 /* Change the code colors based on VSCode exported body classes */
 body.vscode-dark .shiki,
 body.vscode-dark .shiki span {
   color: var(--shiki-dark) !important;
-  background-color: var(--shiki-dark-bg) !important;
+  background-color: transparent !important;
   /* Optional, if you also want font styles */
   font-style: var(--shiki-dark-font-style) !important;
   font-weight: var(--shiki-dark-font-weight) !important;

diff --git a/ide/packages/panoptes/src/Expr.tsx b/ide/packages/panoptes/src/Expr.tsx
@@ -8,16 +8,11 @@ import { makeHighlightPosters } from "@argus/common/func";
 import _ from "lodash";
 import { observer } from "mobx-react";
 import React, { useContext } from "react";
-
 import Code from "./Code";
 import { ObligationFromIdx } from "./Obligation";
 import { CollapsibleElement } from "./TreeView/Directory";
-import { highlightedObligation } from "./signals";
+import { HighlightTargetStore } from "./signals";
 
-/**
- * Expression-level obligations within a `File`. Expects that
- * the `BodyInfoContext` is available.
- */
 const Expr = observer(({ idx }: { idx: ExprIdx }) => {
   const bodyInfo = useContext(BodyInfoContext)!;
   const file = useContext(FileContext)!;
@@ -43,12 +38,10 @@ const Expr = observer(({ idx }: { idx: ExprIdx }) => {
       <ObligationFromIdx idx={oi} key={i} />
     ));
 
-  // TODO: we should limit the length of the expression snippet.
-  // or at the very least syntax highlight it in some way...
-  // I think there should be a better way to represent this information than a blank expr.
-  const header = <Code code={expr.snippet} />;
+  const openChildren = idx === HighlightTargetStore.value?.exprIdx;
 
-  const openChildren = idx === highlightedObligation.value?.exprIdx;
+  // TODO: we should limit the length of the expression snippet or collapse large blocks in some way.
+  const header = <Code code={expr.snippet} />;
 
   return (
     <div onMouseEnter={addHighlight} onMouseLeave={removeHighlight}>

diff --git a/ide/packages/panoptes/src/File.tsx b/ide/packages/panoptes/src/File.tsx
@@ -19,7 +19,7 @@ import React, { Fragment, useContext } from "react";
 import Expr from "./Expr";
 import "./File.css";
 import { CollapsibleElement } from "./TreeView/Directory";
-import { highlightedObligation } from "./signals";
+import { HighlightTargetStore } from "./signals";
 
 const FnIndicator = () => <em>ƒ</em>;
 
@@ -54,7 +54,7 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => {
   const Kids = () =>
     _.map(bodyInfo.exprs(), (i, idx) => <Expr idx={i} key={idx} />);
 
-  const openChildren = bodyInfo.hash === highlightedObligation.value?.bodyIdx;
+  const openChildren = bodyInfo.hash === HighlightTargetStore.value?.bodyIdx;
 
   return (
     <BodyInfoContext.Provider value={bodyInfo}>

diff --git a/ide/packages/panoptes/src/Obligation.tsx b/ide/packages/panoptes/src/Obligation.tsx
@@ -24,7 +24,7 @@ import { CollapsibleElement } from "./TreeView/Directory";
 import { ResultRaw } from "./TreeView/Node";
 import TreeApp from "./TreeView/TreeApp";
 import { WaitingOn } from "./WaitingOn";
-import { highlightedObligation } from "./signals";
+import { HighlightTargetStore } from "./signals";
 
 export const ObligationFromIdx = ({ idx }: { idx: ObligationIdx }) => {
   const bodyInfo = useContext(BodyInfoContext)!;
@@ -78,10 +78,9 @@ const ProofTreeWrapper = ({
 
   useEffect(() => {
     const getData = async () => {
-      const tree = await messageSystem.requestData<"tree">({
+      const tree = await messageSystem.requestData("tree", {
         type: "FROM_WEBVIEW",
         file: file,
-        command: "tree",
         predicate: obligation,
         range: range
       });
@@ -118,13 +117,13 @@ const Obligation = observer(
     );
 
     const isTargetObligation =
-      highlightedObligation.value?.hash === obligation.hash;
+      HighlightTargetStore.value?.hash === obligation.hash;
 
     useLayoutEffect(() => {
-      if (highlightedObligation.value?.hash === obligation.hash) {
+      if (isTargetObligation) {
         ref.current?.scrollIntoView({ behavior: "smooth" });
       }
-    }, []);
+    }, [isTargetObligation]);
 
     const header = (
       <div

diff --git a/ide/packages/panoptes/src/signals.ts b/ide/packages/panoptes/src/signals.ts
@@ -4,7 +4,7 @@ import type { TypeContext } from "@argus/print/context";
 import { action, makeObservable, observable } from "mobx";
 import type { ReactElement } from "react";
 
-class HighlightTargetStore {
+class HighlightTarget {
   value?: ErrorJumpTargetInfo;
 
   constructor() {
@@ -17,6 +17,7 @@ class HighlightTargetStore {
   }
 
   set(info: ErrorJumpTargetInfo) {
+    console.debug("Setting highlight target", info);
     this.value = info;
   }
 
@@ -25,7 +26,7 @@ class HighlightTargetStore {
   }
 }
 
-export const highlightedObligation = new HighlightTargetStore();
+export const HighlightTargetStore = new HighlightTarget();
 
 // MiniBuffer data that should *not* rely on type context
 type DataNoCtx = {
@@ -55,6 +56,7 @@ class MiniBufferData {
     makeObservable(this, {
       data: observable,
       set: action,
+      reset: action,
       pin: action,
       unpin: action
     });

diff --git a/ide/packages/print/src/Attention.css b/ide/packages/print/src/Attention.css
@@ -1,16 +1,19 @@
 @keyframes attention-highlight {
     0% {
+        display: inline-block;
         background-color: transparent;
-        border-width: 100%;
     }
+
     50% {
+        display: inline-block;
         background-color: var(--vscode-editor-findMatchBackground);
-        border-color: var(--vscode-focusBorder);
-        border-width: 150%;
+        border: 2px solid var(--vscode-editor-findMatchBorder);
+        border-radius: 2px;
     }
+
     100% {
+        display: inline-block;
         background-color: transparent;
-        border-width: 100%;
     }
 }
 
@@ -21,7 +24,7 @@
     }
 
     50% {
-        font-size: 115%;
+        font-size: 110%;
         font-weight: bold;
     }
 
@@ -39,5 +42,6 @@ span.Attention {
 
 span.AttentionText {
     display: inline-block;
+    background-color: transparent;
     animation: attention-text 2s ease-in-out;
 }