*: tooltips zIndex

SayaOvO · SayaOvO · commit 1171090e46ad · 2025-11-03T14:25:07.000+08:00
diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx
@@ -37,7 +37,7 @@ export function Tooltip(props_: TooltipProps) {
 
     const adjustedFloatingStyles = {
         ...floatingStyles,
-        zIndex: 10,
+        zIndex: 100,
     }
 
     const logicalDom = React.useContext(LogicalDomContext)

Original file line number	Diff line number	Diff line change
`@@ -37,7 +37,7 @@ export function Tooltip(props_: TooltipProps) {`
`37`	`37`
`38`	`38`	`const adjustedFloatingStyles = {`
`39`	`39`	`...floatingStyles,`
`40`		`- zIndex: 10,`
	`40`	`+ zIndex: 100,`
`41`	`41`	`}`
`42`	`42`
`43`	`43`	`const logicalDom = React.useContext(LogicalDomContext)`