diff --git a/ide/packages/panoptes/src/App.css b/ide/packages/panoptes/src/App.css index e184195..bff7a5d 100644 --- a/ide/packages/panoptes/src/App.css +++ b/ide/packages/panoptes/src/App.css @@ -23,4 +23,5 @@ .DefinitionWrapper.hovered.meta-pressed { color: var(--vscode-editorLink-activeForeground); text-decoration: underline; + cursor: pointer; } \ 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 be58457..206d551 100644 --- a/ide/packages/panoptes/src/TreeView/Directory.tsx +++ b/ide/packages/panoptes/src/TreeView/Directory.tsx @@ -99,15 +99,12 @@ export const DirNode = ({ ); + const info = ( + + {infoChild} + + ); - const info = - Wrappers === undefined ? ( - infoChild - ) : ( - - {infoChild} - - ); const startOpen = startOpenP ? startOpenP(idx) : false; return ( diff --git a/ide/packages/panoptes/src/TreeView/Wrappers.css b/ide/packages/panoptes/src/TreeView/Wrappers.css index 9d122ce..99c3cfc 100644 --- a/ide/packages/panoptes/src/TreeView/Wrappers.css +++ b/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); diff --git a/ide/packages/panoptes/src/TreeView/Wrappers.tsx b/ide/packages/panoptes/src/TreeView/Wrappers.tsx index e1bdf13..3a9d1e1 100644 --- a/ide/packages/panoptes/src/TreeView/Wrappers.tsx +++ b/ide/packages/panoptes/src/TreeView/Wrappers.tsx @@ -33,7 +33,11 @@ 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 ( setHovered(false)} > {children} - {(hovered || active) && ( - - {_.map(wrappers, (W, i) => ( - setActives(a => arrUpdate(a, i, b))} - /> - ))} - - )} + + {_.map(wrappers, (W, i) => ( + setActives(a => arrUpdate(a, i, b))} + /> + ))} + ); }; diff --git a/ide/packages/print/src/Attention.tsx b/ide/packages/print/src/Attention.tsx index 3d6a99e..53e7f05 100644 --- a/ide/packages/print/src/Attention.tsx +++ b/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(null); + useEffect(() => { + setTimeout(() => ref.current?.classList.remove(className), DURATION); + }, []); + + return ( + + {children} + + ); +}; + export const TextEmphasis = ({ children }: React.PropsWithChildren) => ( - {children} + {children} ); const Attention = ({ children }: React.PropsWithChildren) => ( - {children} + {children} ); export default Attention;