Wed, 15 May 2024 17:04:22 +0200 lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;
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;
Wed, 15 May 2024 16:54:39 +0200 lsp: unified PIDE/decorations and dynamic output decorations format;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 15 May 2024 16:54:39 +0200] rev 81039
lsp: unified PIDE/decorations and dynamic output decorations format;
Wed, 15 May 2024 00:11:34 +0200 vscode: changed test_string to "mix" to be consistent with jEdit;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 15 May 2024 00:11:34 +0200] rev 81038
vscode: changed test_string to "mix" to be consistent with jEdit;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip