feat: shift-click to unselect

leanprover · May 23, 2024 · d78023b · d78023b
1 parent 75f511f
commit d78023b
Showing 1 changed file with 9 additions and 2 deletions.
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -159,7 +159,14 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
 
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return (
-        <>
+        <span
+            onClick={e => {
+                if (e.shiftKey) setSelectedLocs([])
+            }}
+            onPointerDown={e => {
+                if (e.shiftKey) e.preventDefault()
+            }}
+        >
             {hasError && (
                 <div className="error" key="errors">
                     Error updating: {error}.
@@ -243,7 +250,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 ) : (
                     'No info found.'
                 ))}
-        </>
+        </span>
     )
 })