fix: position

leanprover-community · May 16, 2024 · ca66ebb · ca66ebb
1 parent fcdc866
commit ca66ebb
Showing 1 changed file with 4 additions and 6 deletions.
diff --git a/widget/src/infoGraph.tsx b/widget/src/infoGraph.tsx
@@ -6,7 +6,6 @@ import { graphviz } from 'd3-graphviz';
 
 interface Node {
   id : string;
-  pos : DocumentPosition
   html : Html;
 }
 
@@ -19,8 +18,7 @@ interface Graph {
 
 export default ({nodes, dot, pos, defaultHtml} : Graph) => {
   const graphRef = useRef<HTMLDivElement>(null);
-  const [infoState, setInfoState] =
-    useState<{ pos : DocumentPosition, html : Html}>({pos : pos, html : defaultHtml});
+  const [infoState, setInfoState] = useState<Html>(defaultHtml);
 
   useEffect(() => {
     const nodeMap = new Map(nodes.map(node => [node.id, node]))
@@ -57,13 +55,13 @@ export default ({nodes, dot, pos, defaultHtml} : Graph) => {
             const node = nodeMap.get(nodeId);
 
             if (node) {
-              setInfoState({ pos : node.pos, html : node.html });
+              setInfoState(node.html);
             };
           });
         });
         d3.select(graphRef.current)
           .on("click", () => {
-            setInfoState({ pos : pos, html : defaultHtml });
+            setInfoState(defaultHtml);
           });
 
       });
@@ -72,7 +70,7 @@ export default ({nodes, dot, pos, defaultHtml} : Graph) => {
   return (
     <div>
       <div ref={graphRef} />
-      <HtmlDisplay pos={infoState.pos} html={infoState.html} />
+      <HtmlDisplay pos={pos} html={infoState} />
     </div>
   );
 }