Fix MobX overflow and expose safe TyValue printing

examples/bevy/Cargo.toml

@@ -6,4 +6,4 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-bevy = "0.10.1"
+bevy = "0.14.0"

examples/bevy/src/main.rs

@@ -3,8 +3,8 @@ use bevy::prelude::*;
 #[derive(Resource)]
 struct Timer(usize);
 
-fn startup_system(_: Timer) {}
+fn run_timer(_: Timer) {}
 
 fn main() {
-  App::new().add_startup_system(startup_system).run();
+  App::new().add_systems(Update, run_timer).run();
 }

ide/packages/panoptes/src/App.tsx

@@ -1,4 +1,4 @@
-import type { DefinedPath } from "@argus/common/bindings";
+import type { DefinedPath, TyVal } from "@argus/common/bindings";
 import {
   createClosedMessageSystem,
   vscodeMessageSystem
@@ -17,11 +17,10 @@ import {
   isSysMsgUnpin
 } from "@argus/common/lib";
 import { IcoComment } from "@argus/print/Icons";
-import Indented from "@argus/print/Indented";
 import {
-  AllowPathTrim,
-  AllowProjectionSubst,
-  DefPathRender
+  DefPathRender,
+  ProjectionPathRender,
+  TyCtxt
 } from "@argus/print/context";
 import { VSCodeCheckbox } from "@vscode/webview-ui-toolkit/react";
 import _ from "lodash";
@@ -30,6 +29,7 @@ import React, { useEffect, useState } from "react";
 
 import "./App.css";
 import type { TypeContext } from "@argus/print/context";
+import { PrintTyValue } from "@argus/print/lib";
 import MiniBuffer from "./MiniBuffer";
 import Workspace from "./Workspace";
 import { MiniBufferDataStore, highlightedObligation } from "./signals";
@@ -126,42 +126,40 @@ const CustomPathRenderer = observer(
   }
 );
 
-const CustomProjectionRender = ({
-  original,
-  projection,
-  ctx
-}: {
-  original: React.ReactElement;
-  projection: React.ReactElement;
-  ctx: TypeContext;
-}) => {
-  const content = (
-    <AllowPathTrim.Provider value={false}>
-      <AllowProjectionSubst.Provider value={false}>
-        <p> This type is from a projection:</p>
-        <p>Projected type:</p>
-        <Indented>{projection}</Indented>
-        <p>Full path:</p>
-        <Indented>{original}</Indented>
-      </AllowProjectionSubst.Provider>
-    </AllowPathTrim.Provider>
-  );
-  const setStore = () =>
-    MiniBufferDataStore.set({ kind: "projection", content, ctx });
-  const resetStore = () => MiniBufferDataStore.reset();
-  return (
-    <>
-      {projection}
-      <span
-        onMouseEnter={setStore}
-        onMouseLeave={resetStore}
-        style={{ verticalAlign: "super", fontSize: "0.25rem" }}
-      >
-        <IcoComment />
-      </span>
-    </>
-  );
-};
+const CustomProjectionRender = observer(
+  ({
+    ctx,
+    original,
+    projection
+  }: {
+    ctx: TypeContext;
+    original: TyVal;
+    projection: TyVal;
+  }) => {
+    const setStore = () =>
+      MiniBufferDataStore.set({
+        kind: "projection",
+        original,
+        projection,
+        ctx
+      });
+    const resetStore = () => MiniBufferDataStore.reset();
+    return (
+      <>
+        <TyCtxt.Provider value={ctx}>
+          <PrintTyValue ty={projection} />
+        </TyCtxt.Provider>
+        <span
+          onMouseEnter={setStore}
+          onMouseLeave={resetStore}
+          style={{ verticalAlign: "super", fontSize: "0.25rem" }}
+        >
+          <IcoComment />
+        </span>
+      </>
+    );
+  }
+);
 
 const App = observer(({ config }: { config: PanoptesConfig }) => {
   const [openFiles, setOpenFiles] = useState(buildInitialData(config));
@@ -215,7 +213,9 @@ const App = observer(({ config }: { config: PanoptesConfig }) => {
         <AppContext.MessageSystemContext.Provider value={messageSystem}>
           <AppContext.ShowHiddenObligationsContext.Provider value={showHidden}>
             <DefPathRender.Provider value={CustomPathRenderer}>
-              <Workspace files={openFiles} reset={resetState} />
+              <ProjectionPathRender.Provider value={CustomProjectionRender}>
+                <Workspace files={openFiles} reset={resetState} />
+              </ProjectionPathRender.Provider>
             </DefPathRender.Provider>
           </AppContext.ShowHiddenObligationsContext.Provider>
         </AppContext.MessageSystemContext.Provider>

ide/packages/panoptes/src/MiniBuffer.tsx

@@ -1,9 +1,14 @@
-import { TyCtxt } from "@argus/print/context";
-import { PrintDefPathFull } from "@argus/print/lib";
+import {
+  AllowPathTrim,
+  AllowProjectionSubst,
+  TyCtxt
+} from "@argus/print/context";
+import { PrintDefPathFull, PrintTyValue } from "@argus/print/lib";
 import { observer } from "mobx-react";
 import React from "react";
 
 import { IcoPinned } from "@argus/print/Icons";
+import Indented from "@argus/print/Indented";
 import { MiniBufferDataStore } from "./signals";
 import "./MiniBuffer.css";
 
@@ -21,21 +26,36 @@ const MiniBuffer = observer(() => {
       <h2>Type Projection</h2>
     ) : null;
   const pinned = data.pinned ? <IcoPinned onClick={unpinClick} /> : null;
-  const Content =
+  const Content = () =>
     data.kind === "path" ? (
       <PrintDefPathFull defPath={data.path} />
     ) : data.kind === "projection" ? (
-      data.content
+      <>
+        <p>The projected type:</p>
+        <Indented>
+          <PrintTyValue ty={data.projection} />
+        </Indented>
+        <p>comes from the definition path:</p>
+        <Indented>
+          <PrintTyValue ty={data.original} />
+        </Indented>
+      </>
     ) : null;
 
   return (
     <>
       <div id="MiniBuffer">
         {pinned}
         {heading}
-        <div className="Data">
-          <TyCtxt.Provider value={data.ctx}>{Content}</TyCtxt.Provider>
-        </div>
+        <AllowPathTrim.Provider value={false}>
+          <AllowProjectionSubst.Provider value={false}>
+            <TyCtxt.Provider value={data.ctx}>
+              <div className="Data">
+                <Content />
+              </div>
+            </TyCtxt.Provider>
+          </AllowProjectionSubst.Provider>
+        </AllowPathTrim.Provider>
       </div>
       <div className="spacer">{"\u00A0"}</div>
     </>

ide/packages/panoptes/src/signals.ts

@@ -1,4 +1,4 @@
-import type { DefinedPath } from "@argus/common/bindings";
+import type { DefinedPath, TyVal } from "@argus/common/bindings";
 import type { ErrorJumpTargetInfo } from "@argus/common/lib";
 import type { TypeContext } from "@argus/print/context";
 import { action, makeObservable, observable } from "mobx";
@@ -36,7 +36,8 @@ export type BufferDataKind = {
     }
   | {
       kind: "projection";
-      content: React.ReactElement;
+      original: TyVal;
+      projection: TyVal;
     }
 );
 

ide/packages/print/src/context.tsx

@@ -1,6 +1,7 @@
 import type { DefinedPath, Ty, TyVal } from "@argus/common/bindings";
 import { createContext } from "react";
 import React, { type ReactElement } from "react";
+import { PrintTyValue } from "./private/ty";
 
 // Change this to true if we want to by default toggle type parameter lists
 export const AllowToggle = createContext(false);
@@ -21,8 +22,8 @@ export const DefPathRender = createContext(
     Head,
     Rest
   }: {
-    fullPath: DefinedPath;
     ctx: TypeContext;
+    fullPath: DefinedPath;
     Head: ReactElement;
     Rest: ReactElement;
   }) => (
@@ -39,8 +40,8 @@ export const ProjectionPathRender = createContext(
     projection: _prj,
     ctx: _ctx
   }: {
-    original: ReactElement;
-    projection: ReactElement;
     ctx: TypeContext;
-  }) => original
+    original: TyVal;
+    projection: TyVal;
+  }) => <PrintTyValue o={original} />
 );

ide/packages/print/src/lib.tsx

@@ -4,7 +4,8 @@ import type {
   GoalData,
   ImplHeader,
   Obligation,
-  Ty
+  Ty,
+  TyVal
 } from "@argus/common/bindings";
 import React from "react";
 import { ErrorBoundary } from "react-error-boundary";
@@ -23,7 +24,10 @@ import {
   PrintGoalPredicate as UnsafePrintGoalPredicate,
   PrintPredicateObligation as UnsafePrintPredicateObligation
 } from "./private/predicate";
-import { PrintTy as UnsafePrintTy } from "./private/ty";
+import {
+  PrintTy as UnsafePrintTy,
+  PrintTyValue as UnsafePrintTyValue
+} from "./private/ty";
 
 // NOTE: please Please PLEASE wrap all printing components in this
 // `PrintWithFallback`. Pretty printing is still a fragile process and
@@ -76,11 +80,9 @@ export const PrintWithFallback = ({
   );
 };
 
-export const PrintTy = ({ ty }: { ty: Ty }) => {
-  return (
-    <PrintWithFallback object={ty} Content={() => <UnsafePrintTy o={ty} />} />
-  );
-};
+export const PrintTy = ({ ty }: { ty: Ty }) => (
+  <PrintWithFallback object={ty} Content={() => <UnsafePrintTy o={ty} />} />
+);
 
 export const PrintObligation = ({ obligation }: { obligation: Obligation }) => {
   const InnerContent = () => (
@@ -91,16 +93,14 @@ export const PrintObligation = ({ obligation }: { obligation: Obligation }) => {
   return <PrintWithFallback object={obligation} Content={InnerContent} />;
 };
 
-export const PrintImplHeader = ({ impl }: { impl: ImplHeader }) => {
-  return (
-    <AllowToggle.Provider value={true}>
-      <PrintWithFallback
-        object={impl}
-        Content={() => <UnsafePrintImplHeader o={impl} />}
-      />
-    </AllowToggle.Provider>
-  );
-};
+export const PrintImplHeader = ({ impl }: { impl: ImplHeader }) => (
+  <AllowToggle.Provider value={true}>
+    <PrintWithFallback
+      object={impl}
+      Content={() => <UnsafePrintImplHeader o={impl} />}
+    />
+  </AllowToggle.Provider>
+);
 
 export const PrintGoal = ({ o }: { o: GoalData }) => {
   const debugString =
@@ -135,21 +135,23 @@ export const PrintExtensionCandidate = ({
   );
 };
 
-export const PrintBodyName = ({ defPath }: { defPath: DefinedPath }) => {
-  return (
-    <PrintWithFallback
-      object={defPath}
-      // Content={() => <UnsafePrintDefPathFull o={defPath} />}
-      Content={() => <UnsafePrintDefPath o={defPath} />}
-    />
-  );
-};
+export const PrintBodyName = ({ defPath }: { defPath: DefinedPath }) => (
+  <PrintWithFallback
+    object={defPath}
+    Content={() => <UnsafePrintDefPath o={defPath} />}
+  />
+);
 
-export const PrintDefPathFull = ({ defPath }: { defPath: DefinedPath }) => {
-  return (
-    <PrintWithFallback
-      object={defPath}
-      Content={() => <UnsafePrintDefPathFull o={defPath} />}
-    />
-  );
-};
+export const PrintDefPathFull = ({ defPath }: { defPath: DefinedPath }) => (
+  <PrintWithFallback
+    object={defPath}
+    Content={() => <UnsafePrintDefPathFull o={defPath} />}
+  />
+);
+
+export const PrintTyValue = ({ ty }: { ty: TyVal }) => (
+  <PrintWithFallback
+    object={ty}
+    Content={() => <UnsafePrintTyValue o={ty} />}
+  />
+);

ide/packages/print/src/private/path.tsx

@@ -60,8 +60,8 @@ export const PrintDefPath = ({ o }: { o: DefinedPath }) => {
   }) => {
     return (
       <PrintCustomDefPath
-        fullPath={o}
         ctx={tyCtxt}
+        fullPath={o}
         Head={<Prefix />}
         Rest={<Rest />}
       />

ide/packages/print/src/private/ty.tsx

@@ -119,32 +119,15 @@ export const PrintTyProjected = ({
   original,
   projection
 }: { original: TyVal; projection: TyVal }) => {
-  const RenderProjection = useContext(ProjectionPathRender);
+  const PrintCustomProjection = useContext(ProjectionPathRender);
   const tyCtx = useContext(TyCtxt)!;
   return (
-    <RenderProjection
-      original={<PrintTyValue o={original} />}
-      projection={<PrintTyValue o={projection} />}
+    <PrintCustomProjection
       ctx={tyCtx}
+      original={original}
+      projection={projection}
     />
   );
-  // const Content = (
-  //   <AllowPathTrim.Provider value={false}>
-  //     <AllowProjectionSubst.Provider value={false}>
-  //       <p> This type is from a projection:</p>
-  //       <p>Projected type:</p>
-  //       <Indented>
-  //         <PrintTyValue o={projection} />
-  //       </Indented>
-  //       <p>Full path:</p>
-  //       <Indented>
-  //         <PrintTyValue o={original} />
-  //       </Indented>
-  //     </AllowProjectionSubst.Provider>
-  //   </AllowPathTrim.Provider>
-  // );
-
-  // return <Comment Child={<PrintTyValue o={projection} />} Content={Content} />;
 };
 
 export const PrintTyValue = ({ o }: { o: TyVal }) => {