Cache panel contents and force rerender on programatic change.

ide/packages/common/src/communication.ts

@@ -97,7 +97,12 @@ export function createClosedMessageSystem(bodies: BodyBundle[]): MessageSystem {
           )
         );
         if (tree === undefined) {
-          console.error("Body", foundBodies, "hash", body.predicate.hash);
+          console.error(
+            "Tree not found in bodies",
+            foundBodies,
+            "hash",
+            body.predicate.hash
+          );
           return reject(new Error("Obligation hash not found in maps"));
         }
 

ide/packages/common/src/func.ts

@@ -15,6 +15,9 @@ import type {
 import type { MessageSystem } from "./communication";
 import type { Filename } from "./lib";
 
+export const arrUpdate = <T>(arr: T[], idx: number, val: T) =>
+  _.map(arr, (v, i) => (i !== idx ? v : val));
+
 export function isObject(x: any): x is object {
   return typeof x === "object" && x !== null;
 }

ide/packages/panoptes/src/App.tsx

@@ -248,8 +248,6 @@ const App = observer(({ config }: { config: PanoptesConfig }) => {
     if (config.target !== undefined) {
       HighlightTargetStore.set(config.target);
     }
-
-    return () => HighlightTargetStore.reset();
   }, [config.target]);
 
   const Navbar = (
@@ -278,11 +276,7 @@ const App = observer(({ config }: { config: PanoptesConfig }) => {
                 <LocationActionable.Provider
                   value={mkLocationActionable(messageSystem)}
                 >
-                  <Workspace
-                    key={HighlightTargetStore.value?.hash ?? 0}
-                    files={openFiles}
-                    reset={resetState}
-                  />
+                  <Workspace files={openFiles} reset={resetState} />
                   <FillScreen />
                 </LocationActionable.Provider>
               </ProjectionPathRender.Provider>

ide/packages/panoptes/src/File.tsx

@@ -21,7 +21,7 @@ import "./File.css";
 import { CollapsibleElement } from "./TreeView/Directory";
 import { HighlightTargetStore } from "./signals";
 
-const FnIndicator = () => <em>ƒ</em>;
+const fnIndicator = <em>ƒ</em>;
 
 const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => {
   if (!bodyInfo.hasVisibleExprs()) {
@@ -43,7 +43,7 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => {
   const header = (
     <>
       <MonoSpace>
-        <FnIndicator />
+        {fnIndicator}
         {"\u00A0"}
         {bodyName}
       </MonoSpace>
@@ -67,35 +67,17 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => {
   );
 });
 
-const File = ({
-  file,
-  osibs
-}: {
+export interface FileProps {
   file: Filename;
   osibs: ObligationsInBody[];
-}) => {
+}
+
+const File = ({ file, osibs }: FileProps) => {
   const showHidden = useContext(AppContext.ShowHiddenObligationsContext);
   const bodyInfos = _.map(
     osibs,
     (osib, idx) => new BodyInfo(osib, idx, showHidden)
   );
-  const bodiesWithVisibleExprs = _.filter(bodyInfos, bi =>
-    bi.hasVisibleExprs()
-  );
-
-  const bodies = _.map(bodiesWithVisibleExprs, (bodyInfo, idx) => (
-    <Fragment key={idx}>
-      {idx > 0 ? <VSCodeDivider /> : null}
-      <TyCtxt.Provider
-        value={{
-          interner: bodyInfo.tyInterner,
-          projections: {}
-        }}
-      >
-        <ObligationBody bodyInfo={bodyInfo} />
-      </TyCtxt.Provider>
-    </Fragment>
-  ));
 
   const noBodiesFound = (
     <ErrorDiv>
@@ -110,9 +92,29 @@ const File = ({
     </ErrorDiv>
   );
 
+  const bodiesWithVisibleExprs = _.filter(bodyInfos, bi =>
+    bi.hasVisibleExprs()
+  );
+
+  if (bodiesWithVisibleExprs.length === 0) {
+    return noBodiesFound;
+  }
+
   return (
     <FileContext.Provider value={file}>
-      {bodies.length > 0 ? bodies : noBodiesFound}
+      {_.map(bodiesWithVisibleExprs, (bodyInfo, idx) => (
+        <Fragment key={idx}>
+          {idx > 0 ? <VSCodeDivider /> : null}
+          <TyCtxt.Provider
+            value={{
+              interner: bodyInfo.tyInterner,
+              projections: {}
+            }}
+          >
+            <ObligationBody bodyInfo={bodyInfo} />
+          </TyCtxt.Provider>
+        </Fragment>
+      ))}
     </FileContext.Provider>
   );
 };

ide/packages/panoptes/src/TreeView/Directory.tsx

@@ -110,10 +110,6 @@ export const DirNode = ({
     );
   const startOpen = startOpenP ? startOpenP(idx) : false;
 
-  if (idx === 0) {
-    console.warn("StartOpen", startOpen);
-  }
-
   return (
     <CollapsibleElement
       info={info}

ide/packages/panoptes/src/TreeView/Panels.tsx

@@ -1,12 +1,12 @@
+import { arrUpdate } from "@argus/common/func";
 import { TextEmphasis } from "@argus/print/Attention";
 import {
   VSCodePanelTab,
   VSCodePanelView,
-  VSCodePanels,
-  VSCodeProgressRing
+  VSCodePanels
 } from "@vscode/webview-ui-toolkit/react";
 import _ from "lodash";
-import React, { Suspense, useState } from "react";
+import React, { useId, useState, useEffect } from "react";
 
 import "./Panels.css";
 
@@ -19,6 +19,33 @@ export interface PanelDescription {
   Content: React.FC;
   tabProps?: TabProps;
   viewProps?: ViewProps;
+  // FIXME: this shouldn't be here, we should require the title to be unique
+  fn?: string;
+}
+
+interface PanelState {
+  activePanel: number;
+  node?: number;
+  programatic?: boolean;
+}
+
+export function usePanelState() {
+  const [state, setState] = useState<PanelState>({ activePanel: 0 });
+  return [state, setState] as const;
+}
+
+// NOTE: we don't expect someone to have more than 15 tabs open...the `VSCodePanels`
+// is tricky to navigate so this would be an issue. But, we should make this robust to track
+// the size of the underlying buffer better. For safety and performance.
+function useStateArray<T>(n = 15) {
+  const [values, setValues] = useState<(T | undefined)[]>(
+    Array.from({ length: n })
+  );
+  const updateValue = (idx: number, value: T | undefined) =>
+    setValues(a => arrUpdate(a, idx, value));
+  const updateAll = (a: (T | undefined)[]) =>
+    setValues(Array.from({ ...a, length: n }));
+  return [values, updateValue, updateAll] as const;
 }
 
 const Panels = ({
@@ -28,35 +55,97 @@ const Panels = ({
   manager?: [number, (n: number) => void, boolean?];
   description: PanelDescription[];
 }) => {
+  const id = useId();
   const [active, setActive, programaticSwitch] = manager || useState(0);
+  const tabId = (n: number) => `tab-${id}-${n}`;
+
+  const [openFiles, setOpenFiles, resetOpenFiles] = useStateArray<string>();
+  const [tabs, setTabs, resetTabs] = useStateArray<React.ReactElement>();
+  const [panels, setPanels, resetPanels] = useStateArray<React.ReactElement>();
+
+  useEffect(() => {
+    console.debug(`Panel(${id}) mounted`);
+    resetOpenFiles(_.map(description, d => d.fn ?? d.title));
+    fullRender();
+  }, []);
+
+  // NOTE: rerenders should not occur if the user clicks on a tab. We cache the
+  // elements in state to avoid this. IFF the change is *programatic*, meaning
+  // some GUI action caused the change, we always want to force a rerender so that
+  // state change visuals are shown.
+  useEffect(() => {
+    console.debug(`Panel(${id}) params changed`, active, programaticSwitch);
+    if (programaticSwitch) {
+      // On a programatic switch only rerender the active tab
+      rerender(active);
+    }
+  }, [active, programaticSwitch]);
+
+  // A change in description should always rerender. `useEffect` compares with `Object.is` which
+  // returns false for the same valued arrays, a simple hash is the concatenation of all panel titles
+  // which is stable across rerenders.
+  const descriptionHash = _.reduceRight(
+    description,
+    (acc, d) => acc + (d.fn ?? d.title),
+    ""
+  );
+  useEffect(() => {
+    console.debug(`Panel(${id}) description changed`);
+    _.forEach(_.zip(openFiles, description), ([file, d], idx) => {
+      if (file === (d?.fn ?? d?.title)) return;
+
+      console.debug("Rerendering due to description change", file, d);
+      setOpenFiles(idx, d?.fn ?? d?.title);
+      rerender(idx, d);
+    });
+  }, [descriptionHash]);
+
+  const TWrapper = ({ idx, str }: { idx: number; str: string }) =>
+    idx === active && programaticSwitch ? (
+      <TextEmphasis>{str}</TextEmphasis>
+    ) : (
+      str
+    );
+
+  const elementsAt = (idx: number, d: PanelDescription) =>
+    [
+      <VSCodePanelTab
+        {...d.tabProps}
+        key={idx}
+        id={tabId(idx)}
+        onClick={() => setActive(idx)}
+      >
+        <TWrapper idx={idx} str={d.title} />
+      </VSCodePanelTab>,
+      <VSCodePanelView {...d.viewProps} key={idx}>
+        <d.Content />
+      </VSCodePanelView>
+    ] as const;
+
+  const rerender = (idx: number, desc?: PanelDescription) => {
+    if (idx < 0 || description.length <= idx) {
+      setTabs(idx, undefined);
+      setPanels(idx, undefined);
+    }
 
-  const tabId = (n: number) => `tab-${n}`;
-  console.warn("Starting panels on", active);
+    const d = desc ?? description[idx];
+    const [t, p] = elementsAt(idx, d);
+    setTabs(idx, t);
+    setPanels(idx, p);
+  };
 
-  const withExtra = _.map(description, (d, idx) => ({
-    ...d,
-    id: tabId(idx),
-    onClick: () => setActive(idx)
-  }));
+  const fullRender = () => {
+    const [ts, ps] = _.unzip(
+      _.map(description, (d, idx) => elementsAt(idx, d))
+    );
+    resetTabs(ts);
+    resetPanels(ps);
+  };
 
   return (
     <VSCodePanels activeid={tabId(active)}>
-      {_.map(withExtra, ({ id, title, onClick, tabProps }, idx) => {
-        const Wrapper =
-          programaticSwitch && active === idx ? TextEmphasis : React.Fragment;
-        return (
-          <VSCodePanelTab {...tabProps} key={idx} id={id} onClick={onClick}>
-            <Wrapper>{title}</Wrapper>
-          </VSCodePanelTab>
-        );
-      })}
-      {_.map(withExtra, ({ Content, viewProps }, idx) => (
-        <VSCodePanelView {...viewProps} key={idx}>
-          <Suspense fallback={<VSCodeProgressRing />}>
-            <Content />
-          </Suspense>
-        </VSCodePanelView>
-      ))}
+      {tabs}
+      {panels}
     </VSCodePanels>
   );
 };

ide/packages/panoptes/src/TreeView/TreeApp.tsx

@@ -1,12 +1,12 @@
 import TreeInfo from "@argus/common/TreeInfo";
-import type { ProofNodeIdx, SerializedTree } from "@argus/common/bindings";
+import type { SerializedTree } from "@argus/common/bindings";
 import { TreeAppContext } from "@argus/common/context";
 import { TyCtxt } from "@argus/print/context";
-import React, { useState } from "react";
+import React from "react";
 
 import BottomUp from "./BottomUp";
 import Erotisi from "./Erotisi";
-import Panels, { type PanelDescription } from "./Panels";
+import Panels, { type PanelDescription, usePanelState } from "./Panels";
 import TopDown from "./TopDown";
 import "./TreeApp.css";
 
@@ -27,8 +27,6 @@ const TreeApp = ({
   tree: SerializedTree | undefined;
   showHidden?: boolean;
 }) => {
-  console.warn("MOUNTING TREE APP");
-
   if (tree === undefined) {
     console.error("Returned tree `undefined`");
     return <ErrorMessage />;
@@ -49,15 +47,7 @@ const TreeApp = ({
   // --------------------------------------
   // State dependent data for tab switching
 
-  const [state, setState] = useState<{
-    activePanel: number;
-    node?: ProofNodeIdx;
-    programatic?: boolean;
-  }>({ activePanel: 0 });
-
-  // Callback passed to the BottomUp panel to jump to the TopDown panel.
-  const jumpBottomUpToTopDown = (n: ProofNodeIdx) =>
-    setState({ activePanel: 1, node: n, programatic: true });
+  const [state, setState] = usePanelState();
 
   const tabs: PanelDescription[] = [
     {
@@ -72,7 +62,14 @@ const TreeApp = ({
     // FIXME: we probably shouldn't hard-code that value here...
     tabs.unshift({
       title: "Bottom Up",
-      Content: () => <BottomUp jumpToTopDown={jumpBottomUpToTopDown} />
+      Content: () => (
+        <BottomUp
+          jumpToTopDown={n =>
+            // Callback passed to the BottomUp panel to jump to the TopDown panel.
+            setState({ activePanel: 1, node: n, programatic: true })
+          }
+        />
+      )
     });
 
     // Push to place this last
@@ -95,7 +92,7 @@ const TreeApp = ({
           <Panels
             manager={[
               state.activePanel,
-              (n: number) => setState({ activePanel: n }),
+              n => setState({ activePanel: n }),
               state.programatic
             ]}
             description={tabs}