fix: don't display popups during mouse selection (#615)

This PR ensures that the tooltip hover popup doesn't trigger while the
primary mouse button is being held to prevent it from popping up while
user are selecting text.

Author: mhuisi

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.8.4",
+    "version": "0.8.5",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",

lean4-infoview/src/infoview/tooltips.tsx

@@ -280,7 +280,9 @@ export function useHoverTooltip(
     }
 
     const onPointerOver = (e: React.PointerEvent<HTMLSpanElement>) => {
-        if (!isModifierHeld(e)) {
+        // eslint-disable-next-line no-bitwise
+        const isSelectionHover = (e.buttons & 1) !== 0
+        if (!isModifierHeld(e) && !isSelectionHover) {
             guardMouseEvent(_ => startShowTimeout(), e)
         }
     }

package-lock.json

@@ -1540,7 +1540,7 @@
         "test": "node ./out/test/suite/runTest.js"
     },
     "dependencies": {
-        "@leanprover/infoview": "~0.8.4",
+        "@leanprover/infoview": "~0.8.5",
         "@leanprover/infoview-api": "~0.7.0",
         "@leanprover/unicode-input": "~0.1.4",
         "@leanprover/unicode-input-component": "~0.1.4",