vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;

--- a/src/Tools/VSCode/src/vscode_main.scala	Tue Jul 09 16:47:48 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala	Wed Jul 17 20:56:27 2024 +0200
@@ -146,6 +146,7 @@
     "editor.fontSize": 18,
     "editor.lineNumbers": "off",
     "editor.renderIndentGuides": false,
+    "editor.renderWhitespace": "none",
     "editor.rulers": [80, 100],
     "editor.unicodeHighlight.ambiguousCharacters": false,
     "extensions.autoCheckUpdates": false,