Remove Attention after first render, jump to def cursor, etc

ide/packages/panoptes/src/App.css

@@ -23,4 +23,5 @@
 .DefinitionWrapper.hovered.meta-pressed {
     color: var(--vscode-editorLink-activeForeground);
     text-decoration: underline;
+    cursor: pointer;
 }

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

@@ -99,15 +99,12 @@ export const DirNode = ({
       <Node node={node} />
     </span>
   );
+  const info = (
+    <WrapNode wrappers={Wrappers ?? []} n={idx}>
+      {infoChild}
+    </WrapNode>
+  );
 
-  const info =
-    Wrappers === undefined ? (
-      infoChild
-    ) : (
-      <WrapNode wrappers={Wrappers} n={idx}>
-        {infoChild}
-      </WrapNode>
-    );
   const startOpen = startOpenP ? startOpenP(idx) : false;
 
   return (

ide/packages/panoptes/src/TreeView/Wrappers.css

@@ -24,12 +24,19 @@
 }
 
 .WrapperBox {
-    display: inline-flex;
+    display: none;
+    padding-left: 0.5em;
+
     flex-direction: row;
     justify-content: space-evenly;
+    align-items: center;
     gap: 0.25em;
 }
 
+.WrapperBox.is-hovered {
+    display: inline-flex;
+}
+
 .WrapperBox i:hover {
     cursor: pointer;
     color: var(--vscode-input-placeholderForeground);

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

@@ -33,25 +33,27 @@ export const WrapNode = ({
 }: React.PropsWithChildren<{ wrappers: InfoWrapper[]; n: ProofNodeIdx }>) => {
   const [hovered, setHovered] = useState(false);
   const [actives, setActives] = useState(Array(wrappers.length).fill(false));
+
   const active = _.some(actives);
+  const className = classNames("WrapperBox", {
+    "is-hovered": hovered || active
+  });
 
   return (
     <span
       onMouseEnter={() => setHovered(true)}
       onMouseLeave={() => setHovered(false)}
     >
       {children}
-      {(hovered || active) && (
-        <span className="WrapperBox">
-          {_.map(wrappers, (W, i) => (
-            <W
-              key={i}
-              n={n}
-              reportActive={b => setActives(a => arrUpdate(a, i, b))}
-            />
-          ))}
-        </span>
-      )}
+      <span className={className}>
+        {_.map(wrappers, (W, i) => (
+          <W
+            key={i}
+            n={n}
+            reportActive={b => setActives(a => arrUpdate(a, i, b))}
+          />
+        ))}
+      </span>
     </span>
   );
 };

ide/packages/print/src/Attention.tsx

@@ -1,13 +1,32 @@
-import React from "react";
+import React, { useEffect, useRef } from "react";
 
 import "./Attention.css";
 
+const DURATION = 1_000;
+const CN = "Attention";
+
+const Attn = ({
+  children,
+  className = CN
+}: React.PropsWithChildren<{ className?: string }>) => {
+  const ref = useRef<HTMLSpanElement>(null);
+  useEffect(() => {
+    setTimeout(() => ref.current?.classList.remove(className), DURATION);
+  }, []);
+
+  return (
+    <span ref={ref} className={className}>
+      {children}
+    </span>
+  );
+};
+
 export const TextEmphasis = ({ children }: React.PropsWithChildren) => (
-  <span className="AttentionText">{children}</span>
+  <Attn className="AttentionText">{children}</Attn>
 );
 
 const Attention = ({ children }: React.PropsWithChildren) => (
-  <span className="Attention">{children}</span>
+  <Attn>{children}</Attn>
 );
 
 export default Attention;