src/Tools/VSCode/extension/media/main.js
changeset 81046 95f650a8ce08
parent 81038 07ed4ce5c6c9
equal deleted inserted replaced
81045:07d25a1830df 81046:95f650a8ce08
    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