Wed, 12 Jun 2024 20:44:10 +0200 added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 20:44:10 +0200] rev 81049
added vscode options tag;
Thu, 30 May 2024 02:43:29 +0200 vscode: tuned;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 30 May 2024 02:43:29 +0200] rev 81048
vscode: tuned;
Thu, 30 May 2024 02:43:24 +0200 lsp: refactored non-html dynamic/state output;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 30 May 2024 02:43:24 +0200] rev 81047
lsp: refactored non-html dynamic/state output;
Mon, 27 May 2024 13:21:15 +0200 vscode: reduced how often symbol width gets measured;
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;
Mon, 27 May 2024 13:20:31 +0200 vscode: IsabelleDejaVuSansMono for state and output panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:20:31 +0200] rev 81045
vscode: IsabelleDejaVuSansMono for state and output panel;
Mon, 27 May 2024 13:18:29 +0200 vscode: added decoration request on file switch;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:18:29 +0200] rev 81044
vscode: added decoration request on file switch;
Mon, 27 May 2024 13:17:09 +0200 lsp: added decoration_request notification;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 27 May 2024 13:17:09 +0200] rev 81043
lsp: added decoration_request notification;
Thu, 16 May 2024 11:59:33 +0200 lsp: added decorations to state updates;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 16 May 2024 11:59:33 +0200] rev 81042
lsp: added decorations to state updates;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 tip