@@ -90,40 +90,38 @@ const char *BeginHeader =
90
90
91
91
const char *JSForCoverage =
92
92
R"javascript(
93
-
94
93
function next_uncovered(selector, reverse, scroll_selector) {
95
94
function visit_element(element) {
96
95
element.classList.add("seen");
97
96
element.classList.add("selected");
98
-
99
- if (!scroll_selector) {
100
- scroll_selector = "tr:has(.selected) td.line-number"
101
- }
102
-
103
- const scroll_to = document.querySelector(scroll_selector);
104
- if (scroll_to) {
105
- scroll_to.scrollIntoView({behavior: "smooth", block: "center", inline: "end"});
106
- }
107
-
97
+
98
+ if (!scroll_selector) {
99
+ scroll_selector = "tr:has(.selected) td.line-number"
100
+ }
101
+
102
+ const scroll_to = document.querySelector(scroll_selector);
103
+ if (scroll_to) {
104
+ scroll_to.scrollIntoView({behavior: "smooth", block: "center", inline: "end"});
105
+ }
108
106
}
109
-
107
+
110
108
function select_one() {
111
109
if (!reverse) {
112
110
const previously_selected = document.querySelector(".selected");
113
-
111
+
114
112
if (previously_selected) {
115
113
previously_selected.classList.remove("selected");
116
114
}
117
-
115
+
118
116
return document.querySelector(selector + ":not(.seen)");
119
- } else {
117
+ } else {
120
118
const previously_selected = document.querySelector(".selected");
121
-
119
+
122
120
if (previously_selected) {
123
121
previously_selected.classList.remove("selected");
124
122
previously_selected.classList.remove("seen");
125
123
}
126
-
124
+
127
125
const nodes = document.querySelectorAll(selector + ".seen");
128
126
if (nodes) {
129
127
const last = nodes[nodes.length - 1]; // last
@@ -133,54 +131,52 @@ function next_uncovered(selector, reverse, scroll_selector) {
133
131
}
134
132
}
135
133
}
136
-
134
+
137
135
function reset_all() {
138
136
if (!reverse) {
139
137
const all_seen = document.querySelectorAll(selector + ".seen");
140
-
138
+
141
139
if (all_seen) {
142
140
all_seen.forEach(e => e.classList.remove("seen"));
143
141
}
144
142
} else {
145
143
const all_seen = document.querySelectorAll(selector + ":not(.seen)");
146
-
144
+
147
145
if (all_seen) {
148
146
all_seen.forEach(e => e.classList.add("seen"));
149
147
}
150
148
}
151
-
149
+
152
150
}
153
-
151
+
154
152
const uncovered = select_one();
155
153
156
154
if (uncovered) {
157
155
visit_element(uncovered);
158
156
} else {
159
157
reset_all();
160
-
161
-
158
+
162
159
const uncovered = select_one();
163
-
160
+
164
161
if (uncovered) {
165
162
visit_element(uncovered);
166
163
}
167
164
}
168
165
}
169
166
170
- function next_line(reverse) {
167
+ function next_line(reverse) {
171
168
next_uncovered("td.uncovered-line", reverse)
172
169
}
173
170
174
- function next_region(reverse) {
171
+ function next_region(reverse) {
175
172
next_uncovered("span.red.region", reverse);
176
173
}
177
174
178
- function next_branch(reverse) {
175
+ function next_branch(reverse) {
179
176
next_uncovered("span.red.branch", reverse);
180
177
}
181
178
182
179
document.addEventListener("keypress", function(event) {
183
- console.log(event);
184
180
const reverse = event.shiftKey;
185
181
if (event.code == "KeyL") {
186
182
next_line(reverse);
@@ -191,7 +187,6 @@ document.addEventListener("keypress", function(event) {
191
187
if (event.code == "KeyR") {
192
188
next_region(reverse);
193
189
}
194
-
195
190
});
196
191
)javascript" ;
197
192
0 commit comments