From cbfde7ddb111d06033d3ca239b112e4c25c9c22d Mon Sep 17 00:00:00 2001
From: j433866 <j433866@gmail.com>
Date: Tue, 7 May 2019 14:33:38 +0100
Subject: [PATCH] Don't highlight if the input and output tab numbers are
 different

---
 src/web/HighlighterWaiter.mjs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/web/HighlighterWaiter.mjs b/src/web/HighlighterWaiter.mjs
index 99ae10b1..dbe420b0 100755
--- a/src/web/HighlighterWaiter.mjs
+++ b/src/web/HighlighterWaiter.mjs
@@ -378,6 +378,8 @@ class HighlighterWaiter {
     displayHighlights(pos, direction) {
         if (!pos) return;
 
+        if (this.manager.input.getActiveTab() !== this.manager.output.getActiveTab()) return;
+
         const io = direction === "forward" ? "output" : "input";
 
         document.getElementById(io + "-selection-info").innerHTML = this.selectionInfo(pos[0].start, pos[0].end);