1 files changed, 16 insertions, 1 deletions
diff --git a/src/new_fields/Doc.ts b/src/new_fields/Doc.ts
index 58304cebb..6acc6e1ca 100644
--- a/src/new_fields/Doc.ts
+++ b/src/new_fields/Doc.ts
@@ -637,7 +637,7 @@ export namespace Doc {
 
     export function isBrushedHighlightedDegree(doc: Doc) {
         if (Doc.IsHighlighted(doc)) {
-            return 3;
+            return 6;
         }
         else {
             return Doc.IsBrushedDegree(doc);
@@ -673,6 +673,21 @@ export namespace Doc {
         return doc;
     }
 
+    export function linkFollowUnhighlight() {
+        Doc.UnhighlightAll();
+        document.removeEventListener("pointerdown", linkFollowUnhighlight);
+    }
+
+    let dt = 0;
+    export function linkFollowHighlight(destDoc: Doc) {
+        linkFollowUnhighlight();
+        Doc.HighlightDoc(destDoc);
+        document.removeEventListener("pointerdown", linkFollowUnhighlight);
+        document.addEventListener("pointerdown", linkFollowUnhighlight);
+        let x = dt = Date.now();
+        window.setTimeout(() => dt == x && linkFollowUnhighlight(), 5000);
+    }
+
     export class HighlightBrush {
         @observable HighlightedDoc: Map<Doc, boolean> = new Map();
     }