diff --git a/core/client.js b/core/client.js index 0b133f68..f74f55fd 100644 --- a/core/client.js +++ b/core/client.js @@ -1662,6 +1662,29 @@ async function sourcePretty() { } } +function toggleVisibleWhitespace() { + let editor_style = document.getElementById('editor_style'); + /* + * There is likely a better way to do this, but stomping on the CSS was + * the easiest to wrangle at the time. + */ + if (editor_style.innerHTML.length) { + editor_style.innerHTML = ''; + } else { + editor_style.innerHTML = css` + .cm-trailingSpace { + background-color: unset !important; + } + .cm-highlightTab { + background-image: unset !important; + } + .cm-highlightSpace:before { + content: unset !important; + } + `; + } +} + // TODOC window.addEventListener('load', function () { window.addEventListener('hashchange', hashChange); @@ -1687,6 +1710,9 @@ window.addEventListener('load', function () { document .getElementById('pretty') .addEventListener('click', () => sourcePretty()); + document + .getElementById('whitespace') + .addEventListener('click', () => toggleVisibleWhitespace()); document .getElementById('trace_button') .addEventListener('click', function (event) { diff --git a/core/index.html b/core/index.html index 35c21521..3229a7f8 100644 --- a/core/index.html +++ b/core/index.html @@ -57,7 +57,7 @@ class="w3-bar-item w3-button w3-blue" id="icon" name="icon" - accesskey="i" + accesskey="j" onmouseover="set_access_key_title(event)" data-tip="Set an icon/emoji for the app" > @@ -93,6 +93,16 @@ > 🧼 +
+