equal
deleted
inserted
replaced
23 const locate_button = document.getElementById('locate_button'); |
23 const locate_button = document.getElementById('locate_button'); |
24 locate_button && locate_button.addEventListener('click', e => { |
24 locate_button && locate_button.addEventListener('click', e => { |
25 vscode.postMessage({'command': 'locate'}); |
25 vscode.postMessage({'command': 'locate'}); |
26 }); |
26 }); |
27 |
27 |
|
28 const test_string = "mix"; |
|
29 const test_span = document.createElement("span"); |
|
30 test_span.textContent = test_string; |
|
31 document.body.appendChild(test_span); |
|
32 const symbol_width = test_span.getBoundingClientRect().width / test_string.length; |
|
33 document.body.removeChild(test_span); |
|
34 |
28 const get_window_margin = () => { |
35 const get_window_margin = () => { |
29 const test_string = "mix"; |
|
30 const test_span = document.createElement("span"); |
|
31 test_span.textContent = test_string; |
|
32 document.body.appendChild(test_span); |
|
33 const symbol_width = test_span.getBoundingClientRect().width / test_string.length; |
|
34 document.body.removeChild(test_span); |
|
35 |
|
36 const width = window.innerWidth / symbol_width; |
36 const width = window.innerWidth / symbol_width; |
37 const result = Math.max(width - 16, 1); // extra headroom |
37 const result = Math.max(width - 16, 1); // extra headroom |
38 return result; |
38 return result; |
39 } |
39 } |
40 |
40 |