Address review comments

Implement a brief hysteresis also on the dismissal of the hover pop-up
on mouse movement out of the target element so that

(a) the user has an opportunity to mouse over the pop-up itself to
    interact with it, clicking links, hitting buttons, copying text
(b) not dismiss the pop-up until the mouse pointer stops moving (helps
    accessibility for those with pointer accuracy challenges)

The previous commit also had a misunderstanding of the the disposable
returned by the DisposableCollection::push() method, that it would also
dispose the original disposable, but it doesn't. Reworking disposable
management fixed other issues in which transitioning to another hover
target sometimes would not pop up.

Signed-off-by: Christian W. Damus <[email protected]>

Author: cdamus

packages/core/src/browser/hover-service.ts

@@ -25,6 +25,10 @@ import '../../src/browser/style/hover-service.css';
 
 export type HoverPosition = 'left' | 'right' | 'top' | 'bottom';
 
+// Threshold, in milliseconds, over which a mouse movement is not considered
+// quick enough as to be ignored
+const quickMouseThresholdMillis = 200;
+
 export namespace HoverPosition {
     export function invertIfNecessary(position: HoverPosition, target: DOMRect, host: DOMRect, totalWidth: number, totalHeight: number): HoverPosition {
         if (position === 'left') {
@@ -91,31 +95,36 @@ export class HoverService {
         }
         return this._hoverHost;
     }
+
+    // Pending presentation of the hover pop-up
     protected pendingTimeout: Disposable | undefined;
-    protected pendingHoverCancellation: Disposable | undefined;
+    // Pending cancellation of presentation of the hover pop-up or
+    // dismissal of the hover pop-up currently presented
+    protected pendingHoverCancel: Disposable | undefined;
     protected hoverTarget: HTMLElement | undefined;
     protected lastHidHover = Date.now();
     protected readonly disposeOnHide = new DisposableCollection();
 
     requestHover(request: HoverRequest): void {
         if (request.target !== this.hoverTarget) {
+            this.pendingHoverCancel?.dispose();
             this.cancelHover();
             const hoverDelay = this.getHoverDelay();
             this.pendingTimeout = disposableTimeout(() => this.renderHover(request), hoverDelay);
             if (hoverDelay > 0) {
-                this.cancelHoverOnMouseOut(request);
+                this.cancelPendingHoverOnMouseOut(request);
             }
         }
     }
 
     protected getHoverDelay(): number {
-        return Date.now() - this.lastHidHover < 200
+        return Date.now() - this.lastHidHover < quickMouseThresholdMillis
             ? 0
             : this.preferences.get('workbench.hover.delay', isOSX ? 1500 : 500);
     }
 
     protected async renderHover(request: HoverRequest): Promise<void> {
-        this.cancelPendingHoverCancellation();
+        this.pendingHoverCancel?.dispose();
 
         const host = this.hoverHost;
         let firstChild: HTMLElement | undefined;
@@ -201,36 +210,41 @@ export class HoverService {
         return position;
     }
 
-    /** Cancel the pending cancellation of hover. */
-    protected cancelPendingHoverCancellation(): void {
-        this.pendingHoverCancellation?.dispose();
-        this.pendingHoverCancellation = undefined;
-    }
-
     protected listenForMouseOut(): void {
         const handleMouseMove = (e: MouseEvent) => {
             if (e.target instanceof Node && !this.hoverHost.contains(e.target) && !this.hoverTarget?.contains(e.target)) {
-                this.cancelHover();
+                this.pendingHoverCancel?.dispose();
+                this.pendingHoverCancel = disposableTimeout(() => {
+                    if (!this.hoverHost.matches(':hover')) {
+                        this.cancelHover();
+                    }
+                }, quickMouseThresholdMillis);
+                this.disposeOnHide.push(this.pendingHoverCancel);
             }
         };
         document.addEventListener('mousemove', handleMouseMove);
         this.disposeOnHide.push({ dispose: () => document.removeEventListener('mousemove', handleMouseMove) });
     }
 
-    protected cancelHoverOnMouseOut(request: HoverRequest): void {
-        this.cancelPendingHoverCancellation();
+    protected cancelPendingHoverOnMouseOut(request: HoverRequest): void {
+        this.pendingHoverCancel?.dispose();
         const target = request.target;
         const handleMouseLeave = (): void => {
-            this.cancelHover();
-            this.cancelPendingHoverCancellation();
+            // Cancel the pending hover if it hasn't yet been presented
+            if (!this.hoverHost.isConnected) {
+                this.cancelHover();
+            }
+            this.pendingHoverCancel?.dispose();
         };
         target.addEventListener('mouseleave', handleMouseLeave);
-        this.pendingHoverCancellation = this.disposeOnHide.push(
-            Disposable.create(() => target.removeEventListener('mouseleave', handleMouseLeave)));
+        this.pendingHoverCancel = Disposable.create(
+            () => target.removeEventListener('mouseleave', handleMouseLeave));
+        this.disposeOnHide.push(this.pendingHoverCancel);
     }
 
     cancelHover(): void {
         this.pendingTimeout?.dispose();
+        this.pendingHoverCancel?.dispose();
         this.unRenderHover();
         this.disposeOnHide.dispose();
         this.hoverTarget = undefined;