Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 30 May 2024 02:43:24 +0200] rev 81047
lsp: refactored non-html dynamic/state output;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:21:15 +0200] rev 81046
vscode: reduced how often symbol width gets measured;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:20:31 +0200] rev 81045
vscode: IsabelleDejaVuSansMono for state and output panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:18:29 +0200] rev 81044
vscode: added decoration request on file switch;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:17:09 +0200] rev 81043
lsp: added decoration_request notification;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 16 May 2024 11:59:33 +0200] rev 81042
lsp: added decorations to state updates;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 16 May 2024 11:59:06 +0200] rev 81041
lsp: added delay to dynamic_output updates after a set_margin;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 15 May 2024 17:04:22 +0200] rev 81040
lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;