From 656eb584c8ab79c949cc90f2a82b3fe79756714c Mon Sep 17 00:00:00 2001
From: Will Crichton <wcrichto@cs.stanford.edu>
Date: Thu, 21 Mar 2024 16:26:36 -0700
Subject: [PATCH] Improve styling of hierarchical and graph views of trees

---
 Cargo.lock                                    |  4 +-
 ide/packages/panoptes/src/File.css            |  5 --
 ide/packages/panoptes/src/File.tsx            |  6 +-
 ide/packages/panoptes/src/Icons.css           | 12 ++++
 ide/packages/panoptes/src/Icons.tsx           |  6 +-
 .../panoptes/src/TreeView/BottomUp.tsx        | 16 ++---
 .../panoptes/src/TreeView/Directory.css       | 39 +++++++------
 .../panoptes/src/TreeView/Directory.tsx       | 58 ++++++++-----------
 ide/packages/panoptes/src/TreeView/Graph.tsx  | 15 +++--
 ide/packages/panoptes/src/TreeView/Node.tsx   |  6 +-
 .../panoptes/src/TreeView/TopDown.tsx         | 37 ++++++------
 .../panoptes/src/TreeView/TreeApp.css         |  4 +-
 .../panoptes/src/TreeView/TreeCycle.tsx       |  6 +-
 .../panoptes/src/print/private/ty.tsx         |  6 +-
 14 files changed, 112 insertions(+), 108 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index cba523b..492e502 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -25,7 +25,7 @@ checksum = "080e9890a082662b09c1ad45f567faeeb47f22b5fb23895fbe1e651e718e25ca"
 
 [[package]]
 name = "argus-cli"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "anyhow",
  "argus-lib",
@@ -41,7 +41,7 @@ dependencies = [
 
 [[package]]
 name = "argus-lib"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "anyhow",
  "argus-lib",
diff --git a/ide/packages/panoptes/src/File.css b/ide/packages/panoptes/src/File.css
index 34389af..26563d6 100644
--- a/ide/packages/panoptes/src/File.css
+++ b/ide/packages/panoptes/src/File.css
@@ -1,8 +1,3 @@
-.ObligationCard {
-    display: block;
-    width: 100%;
-}
-
 span.ErrorCount {
     color: var(--vscode-errorForeground);
 }
diff --git a/ide/packages/panoptes/src/File.tsx b/ide/packages/panoptes/src/File.tsx
index 7c5ba1b..a4067d8 100644
--- a/ide/packages/panoptes/src/File.tsx
+++ b/ide/packages/panoptes/src/File.tsx
@@ -99,7 +99,7 @@ const ObligationCard = observer(
   ({ range, obligation }: { range: CharRange; obligation: Obligation }) => {
     const file = useContext(FileContext)!;
     const id = obligationCardId(file, obligation.hash);
-    const ref = useRef<HTMLSpanElement>(null);
+    const ref = useRef<HTMLDivElement>(null);
 
     const [addHighlight, removeHighlight] = makeHighlightPosters(
       obligation.range,
@@ -119,7 +119,7 @@ const ObligationCard = observer(
     }, []);
 
     const header = (
-      <span
+      <div
         id={id}
         className={className}
         ref={ref}
@@ -128,7 +128,7 @@ const ObligationCard = observer(
       >
         <ResultRaw result={obligation.result} />
         <PrintObligation obligation={obligation} />
-      </span>
+      </div>
     );
 
     return (
diff --git a/ide/packages/panoptes/src/Icons.css b/ide/packages/panoptes/src/Icons.css
index bc18678..0274433 100644
--- a/ide/packages/panoptes/src/Icons.css
+++ b/ide/packages/panoptes/src/Icons.css
@@ -4,4 +4,16 @@
 
   padding-right: 0.2em;
   padding-left: 0.2em;
+}
+
+.codicon-error {
+  color: var(--vscode-errorForeground);
+}
+
+.codicon-question {
+  color: var(--vscode-inputValidation-warningBorder);
+}
+
+.codicon-check {
+  color: var(--vscode-inputValidation-infoBorder);
 }
\ No newline at end of file
diff --git a/ide/packages/panoptes/src/Icons.tsx b/ide/packages/panoptes/src/Icons.tsx
index 45d7029..427cc74 100644
--- a/ide/packages/panoptes/src/Icons.tsx
+++ b/ide/packages/panoptes/src/Icons.tsx
@@ -42,6 +42,6 @@ export const IcoNote = () => <i className="codicon codicon-note" />;
 
 export const IcoMegaphone = () => <i className="codicon codicon-megaphone" />;
 
-export const IcoTreeDown = () => (
-  <i className="codicon codicon-type-hierarchy-sub" />
-);
+export const IcoTreeDown: React.FC<
+  React.HTMLAttributes<HTMLElement>
+> = props => <i className="codicon codicon-type-hierarchy-sub" {...props} />;
diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx
index 10536d6..34d9b80 100644
--- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx
+++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx
@@ -150,11 +150,7 @@ const BottomUp = () => {
   });
 
   const LeafElement = ({ leaf }: { leaf: TreeViewWithRoot }) => (
-    <DirRecursive
-      level={[leaf.root]}
-      getNext={mkGetChildren(leaf)}
-      styleEdges={false}
-    />
+    <DirRecursive level={[leaf.root]} getNext={mkGetChildren(leaf)} />
   );
 
   const recommendedSortedViews = tree.sortByRecommendedOrder(
@@ -169,13 +165,9 @@ const BottomUp = () => {
     others.length === 0 ? null : (
       <CollapsibleElement
         info={<span>Other failures ...</span>}
-        Children={() => (
-          <>
-            {_.map(others, (leaf, i) => (
-              <LeafElement key={i} leaf={leaf} />
-            ))}
-          </>
-        )}
+        Children={() =>
+          _.map(others, (leaf, i) => <LeafElement key={i} leaf={leaf} />)
+        }
       />
     );
 
diff --git a/ide/packages/panoptes/src/TreeView/Directory.css b/ide/packages/panoptes/src/TreeView/Directory.css
index 9cc8590..911d545 100644
--- a/ide/packages/panoptes/src/TreeView/Directory.css
+++ b/ide/packages/panoptes/src/TreeView/Directory.css
@@ -1,7 +1,3 @@
-.DirRecursive {
-    line-height: 2;
-}
-
 .DirRecursive.is-candidate {
     border-left: 1px dotted var(--vscode-dropdown-border);
 }
@@ -14,15 +10,15 @@
     border-left: 1px solid var(--vscode-widget-border);
 }
 
-.Collapsible {
+.DirNodeChildren {
     height: auto;
 }
 
-.Collapsible.indent {
-    padding-left: 0.5em;
+.DirNodeChildren.indent {
+    padding-left: 15px;
 }
 
-.Collapsible.collapsed {
+.DirNodeChildren.collapsed {
     height: 0;
     overflow: hidden;
 }
@@ -30,28 +26,35 @@
 .DirNode {
     font-family: Menlo, Monaco, "Courier New", monospace;
     display: flex;
-    flex-direction: row;
-    gap: 1.00em;
+    flex-direction: column;    
+    gap: 10px;
 }
 
 .DirNode.WhereConstraintArea {
-    flex-direction: column;
-    gap: 0;
+    flex-direction: column;    
+}
+
+.DirNodeLabel {
+    display: flex;    
 }
 
-.DirNode > .toggle {
-    display: inline-block;
-    width: 10px;
+.DirNodeLabel > .toggle {
+    cursor: pointer;
 }
 
-.DirNode > .toggle > .codicon {
+.DirNodeLabel > .toggle .codicon {
     font-size: 10px;
 }
 
-.information > pre {
+.DirNodeLabel > .label .codicon {
+    font-size: 14px;
+    margin-right: 3px;
+}
+
+.DirNodeLabel > .label > pre {
     margin-top: 0;
 }
 
-.information::before {
+.DirNodeLabel > .label::before {
     content: ' ';
 }
\ No newline at end of file
diff --git a/ide/packages/panoptes/src/TreeView/Directory.tsx b/ide/packages/panoptes/src/TreeView/Directory.tsx
index 605d549..133c420 100644
--- a/ide/packages/panoptes/src/TreeView/Directory.tsx
+++ b/ide/packages/panoptes/src/TreeView/Directory.tsx
@@ -51,45 +51,54 @@ export const CollapsibleElement = ({
 
   const toggleCollapse = (e: React.MouseEvent<HTMLElement>) => {
     e.preventDefault();
+    e.stopPropagation();
     setIsOpen(!isOpen);
   };
 
-  const collapseCN = classNames("Collapsible", {
+  const collapseCN = classNames("DirNodeChildren", {
     indent: indentChildren,
     collapsed: !isOpen,
   });
 
   return (
-    <>
-      <div className="DirNode" onClick={toggleCollapse}>
+    <div className="DirNode">
+      <div className="DirNodeLabel" onClick={toggleCollapse}>
         <div className="toggle">
           {Children !== null ? (isOpen ? openIco : closedIco) : null}
         </div>
-        <span className="information">{info}</span>
+        <div className="label">{info}</div>
       </div>
-      <div className={collapseCN}>{children ?? null}</div>
-    </>
+      <div className={collapseCN}>{children}</div>
+    </div>
   );
 };
 
-type InfoWrapper = React.FC<{ n: ProofNodeIdx; Child: React.FC }>;
+export type InfoWrapper = React.FC<{
+  n: ProofNodeIdx;
+  Child: React.ReactElement;
+}>;
+export interface TreeRenderParams {
+  Wrapper?: InfoWrapper;
+  styleEdges?: boolean;
+}
+export let TreeRenderContext = React.createContext<TreeRenderParams>({});
 
 export const DirNode = ({
   idx,
   Children,
-  Wrapper = ({ n: _, Child }) => <Child />,
 }: {
   idx: number;
   Children: React.FC | null;
-  Wrapper: InfoWrapper;
 }) => {
   const tree = useContext(TreeContext)!;
+  const { Wrapper } = useContext(TreeRenderContext);
   const node = tree.node(idx);
 
   const arrows: ElementPair = [<IcoTriangleDown />, <IcoTriangleRight />];
   const dots: ElementPair = [<IcoDot />, <IcoDot />];
   const icons = "Result" in node ? dots : arrows;
-  const info = <Wrapper n={idx} Child={() => <Node node={node} />} />;
+  const infoChild = <Node node={node} />;
+  const info = Wrapper ? <Wrapper n={idx} Child={infoChild} /> : infoChild;
 
   return (
     <CollapsibleElement
@@ -104,15 +113,12 @@ export const DirNode = ({
 export const DirRecursive = ({
   level,
   getNext,
-  styleEdges,
-  Wrapper = ({ n: _, Child }) => <Child />,
 }: {
   level: ProofNodeIdx[];
   getNext: (idx: ProofNodeIdx) => ProofNodeIdx[];
-  styleEdges: boolean;
-  Wrapper?: InfoWrapper;
 }) => {
   const tree = useContext(TreeContext)!;
+  const { styleEdges } = useContext(TreeRenderContext);
   const node = tree.node(level[0]);
   const className = classNames("DirRecursive", {
     "is-candidate": styleEdges && "Candidate" in node,
@@ -124,25 +130,11 @@ export const DirRecursive = ({
     <div className={className}>
       {_.map(level, (current, i) => {
         const next = getNext(current);
-        return (
-          <DirNode
-            key={i}
-            idx={current}
-            Wrapper={Wrapper}
-            Children={
-              next.length > 0
-                ? () => (
-                    <DirRecursive
-                      level={next}
-                      getNext={getNext}
-                      styleEdges={styleEdges}
-                      Wrapper={Wrapper}
-                    />
-                  )
-                : null
-            }
-          />
-        );
+        const Children =
+          next.length > 0
+            ? () => <DirRecursive level={next} getNext={getNext} />
+            : null;
+        return <DirNode key={i} idx={current} Children={Children} />;
       })}
     </div>
   );
diff --git a/ide/packages/panoptes/src/TreeView/Graph.tsx b/ide/packages/panoptes/src/TreeView/Graph.tsx
index 457af28..93a8ee9 100644
--- a/ide/packages/panoptes/src/TreeView/Graph.tsx
+++ b/ide/packages/panoptes/src/TreeView/Graph.tsx
@@ -13,7 +13,7 @@ import Tree, { Orientation, TreeLinkDatum, TreeNodeDatum } from "react-d3-tree";
 
 import { TreeContext } from "./Context";
 import "./Graph.css";
-import { Node } from "./Node";
+import { Node, Result } from "./Node";
 import { TreeInfo } from "./TreeInfo";
 
 const useCenteredTree = (
@@ -97,7 +97,11 @@ const TreeNode = ({
         height="100%"
       >
         <span ref={ref} className="foreign-wrapper">
-          <Node node={node} />
+          {"Result" in node ? (
+            <Result idx={node.Result} />
+          ) : (
+            <Node node={node} />
+          )}
         </span>
       </foreignObject>
     </g>
@@ -131,9 +135,7 @@ const Graph = ({ root }: { root: ProofNodeIdx }) => {
   const topology = treeInfo.topology;
   const data = topologyToTreeData(topology, root);
 
-  const customRender = (rd3tProps: any) => {
-    return <TreeNode {...rd3tProps} />;
-  };
+  const customRender = (rd3tProps: any) => <TreeNode {...rd3tProps} />;
 
   const nodeSize = { x: 250, y: 100 };
 
@@ -141,11 +143,12 @@ const Graph = ({ root }: { root: ProofNodeIdx }) => {
     <div className="TreeArea" ref={containerRef}>
       <Tree
         data={data}
-        orientation="vertical"
+        orientation="horizontal"
         translate={translate}
         nodeSize={nodeSize}
         renderCustomNodeElement={customRender}
         pathClassFunc={getEdgeClass(treeInfo)}
+        separation={{ siblings: 1, nonSiblings: 1 }}
       />
     </div>
   );
diff --git a/ide/packages/panoptes/src/TreeView/Node.tsx b/ide/packages/panoptes/src/TreeView/Node.tsx
index 086ccf6..9424a3c 100644
--- a/ide/packages/panoptes/src/TreeView/Node.tsx
+++ b/ide/packages/panoptes/src/TreeView/Node.tsx
@@ -62,7 +62,11 @@ export const Candidate = ({ idx }: { idx: CandidateIdx }) => {
 export const Node = ({ node }: { node: NodeTy }) => {
   const treeInfo = useContext(TreeContext)!;
   if ("Result" in node) {
-    return <Result idx={node.Result} />;
+    return (
+      <>
+        <Result idx={node.Result} /> (end of tree)
+      </>
+    );
   } else if ("Goal" in node) {
     const goal = treeInfo.goal(node.Goal);
     return (
diff --git a/ide/packages/panoptes/src/TreeView/TopDown.tsx b/ide/packages/panoptes/src/TreeView/TopDown.tsx
index 8f54a0c..7fb0eaf 100644
--- a/ide/packages/panoptes/src/TreeView/TopDown.tsx
+++ b/ide/packages/panoptes/src/TreeView/TopDown.tsx
@@ -15,7 +15,7 @@ import React, { useContext, useState } from "react";
 
 import { IcoTreeDown } from "../Icons";
 import { TreeContext } from "./Context";
-import { DirRecursive } from "./Directory";
+import { DirRecursive, TreeRenderContext, TreeRenderParams } from "./Directory";
 import Graph from "./Graph";
 import "./TopDown.css";
 
@@ -24,7 +24,7 @@ export const WrapTreeIco = ({
   Child,
 }: {
   n: ProofNodeIdx;
-  Child: React.FC;
+  Child: React.ReactElement;
 }) => {
   const [isHovered, setIsHovered] = useState(false);
   const [isOpen, setIsOpen] = useState(false);
@@ -47,13 +47,15 @@ export const WrapTreeIco = ({
       onMouseEnter={() => setIsHovered(true)}
       onMouseLeave={() => setIsHovered(false)}
     >
-      <Child />
+      {Child}
       <span
         className="tree-toggle"
         ref={refs.setReference}
         {...getReferenceProps()}
       >
-        {(isHovered || isOpen) && <IcoTreeDown />}
+        <IcoTreeDown
+          style={{ visibility: isHovered || isOpen ? "visible" : "hidden" }}
+        />
       </span>
       {isOpen && (
         <FloatingPortal>
@@ -76,17 +78,16 @@ export const WrapTreeIco = ({
 const TopDown = () => {
   const tree = useContext(TreeContext)!;
 
-  const getGoalChildren = (kids: ProofNodeIdx[]) => {
-    // Sort the candidates by the #infer vars / height of the tree
-    return _.sortBy(kids, k => {
+  // Sort the candidates by the #infer vars / height of the tree
+  const getGoalChildren = (kids: ProofNodeIdx[]) =>
+    _.sortBy(kids, k => {
       const inferVars = tree.inferVars(k);
       const height = tree.maxHeigh(k);
       return inferVars / height;
     });
-  };
 
-  const getCandidateChildren = (kids: ProofNodeIdx[]) => {
-    return _.sortBy(
+  const getCandidateChildren = (kids: ProofNodeIdx[]) =>
+    _.sortBy(
       kids,
       k => {
         switch (tree.result(k) ?? "yes") {
@@ -105,7 +106,6 @@ const TopDown = () => {
         "Goal" in node && tree.goal(node.Goal).isMainTv ? 1 : 0;
       }
     );
-  };
 
   const getChildren = (idx: ProofNodeIdx) => {
     const node = tree.node(idx);
@@ -118,13 +118,16 @@ const TopDown = () => {
       return [];
     }
   };
+
+  let renderParams: TreeRenderParams = {
+    Wrapper: WrapTreeIco,
+    styleEdges: true,
+  };
+
   return (
-    <DirRecursive
-      level={[tree.root]}
-      getNext={getChildren}
-      styleEdges={true}
-      Wrapper={WrapTreeIco}
-    />
+    <TreeRenderContext.Provider value={renderParams}>
+      <DirRecursive level={[tree.root]} getNext={getChildren} />
+    </TreeRenderContext.Provider>
   );
 };
 
diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.css b/ide/packages/panoptes/src/TreeView/TreeApp.css
index 27931bd..8f424f0 100644
--- a/ide/packages/panoptes/src/TreeView/TreeApp.css
+++ b/ide/packages/panoptes/src/TreeView/TreeApp.css
@@ -1,6 +1,6 @@
 .App {
-  width: 100vw;
-  height: 100vh;
+  /* width: 100vw;
+  height: 100vh; */
   display: grid;
   /* grid-template-areas: 
       "tree-interact tree-interact node-info"
diff --git a/ide/packages/panoptes/src/TreeView/TreeCycle.tsx b/ide/packages/panoptes/src/TreeView/TreeCycle.tsx
index 085cbda..4c0bd31 100644
--- a/ide/packages/panoptes/src/TreeView/TreeCycle.tsx
+++ b/ide/packages/panoptes/src/TreeView/TreeCycle.tsx
@@ -3,7 +3,7 @@ import _ from "lodash";
 import React, { useContext } from "react";
 
 import { TreeContext } from "./Context";
-import { DirRecursive } from "./Directory";
+import { DirRecursive, TreeRenderContext } from "./Directory";
 
 const TreeCycle = ({ path }: { path: ProofCycle }) => {
   const tree = useContext(TreeContext)!;
@@ -18,7 +18,9 @@ const TreeCycle = ({ path }: { path: ProofCycle }) => {
   };
 
   return (
-    <DirRecursive level={[tree.root]} getNext={getChildren} styleEdges={true} />
+    <TreeRenderContext.Provider value={{ styleEdges: true }}>
+      <DirRecursive level={[tree.root]} getNext={getChildren} />
+    </TreeRenderContext.Provider>
   );
 };
 
diff --git a/ide/packages/panoptes/src/print/private/ty.tsx b/ide/packages/panoptes/src/print/private/ty.tsx
index de4d1cc..c77adeb 100644
--- a/ide/packages/panoptes/src/print/private/ty.tsx
+++ b/ide/packages/panoptes/src/print/private/ty.tsx
@@ -313,10 +313,8 @@ export const PrintFnDef = ({ o }: { o: FnDef }) => {
   // We should show both (somehow), not sure what's the best way to present it.
   return (
     <>
-      <Toggle summary=".." Children={() => <PrintPolyFnSig o={o.sig} />} />{" "}
-      <CBraced>
-        <PrintDefPath o={o.path} />
-      </CBraced>
+      <PrintDefPath o={o.path} />{" "}
+      <Toggle summary=".." Children={() => <PrintPolyFnSig o={o.sig} />} />
     </>
   );
 };