Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 13:51:45 +0200] rev 81087
updated vscode_extension;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 13:50:01 +0200] rev 81086
NEWS and CONTRIBUTORS;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 10:51:11 +0200] rev 81085
clarified: add operation;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 10:39:32 +0200] rev 81084
minor tuning;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 19 Jul 2024 17:08:20 +0200] rev 81083
lsp: added additional commit characters to immediate completions;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 18 Jul 2024 23:02:49 +0200] rev 81082
vscode: further adjusted default settings and wordPattern for consistent completion popups;
for some reason wordPattern must be set to match (almost) everything, otherwise completions only pop up every other character, and then we must disable wordBasedSuggestions or it will suggest whole lines out of the document;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 18 Jul 2024 17:59:50 +0200] rev 81081
lsp: added more triggerCharacters to make completion popups more consistent;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 18 Jul 2024 01:18:43 +0200] rev 81080
vscode: added default setting to make completions pop up by themselves;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 18 Jul 2024 22:08:46 +0200] rev 81079
lsp: improved completions;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 17 Jul 2024 21:03:56 +0200] rev 81078
vscode: removed unused code;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 17 Jul 2024 21:02:30 +0200] rev 81077
vscode: removed README because its content is outdated;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 17 Jul 2024 20:56:27 +0200] rev 81076
vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;
Thomas Lindae <thomas.lindae@in.tum.de> [Tue, 09 Jul 2024 16:47:48 +0200] rev 81075
lsp: added symbol conversion request;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 05 Jul 2024 21:40:39 +0200] rev 81074
vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 05 Jul 2024 13:30:07 +0200] rev 81073
vscode: removed unused import;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 05 Jul 2024 13:16:47 +0200] rev 81072
vscode: changed vscode_unicode_symbols_edits option default to true;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 05 Jul 2024 13:15:50 +0200] rev 81071
vscode: made uri equality check on actual strings, not on the functions;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 05 Jul 2024 13:15:05 +0200] rev 81070
vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
disabled decoration requests as decoration caching is already done on client-side;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 01 Jul 2024 04:34:04 +0200] rev 81069
lsp: added rudimentary indenting to code actions;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 01 Jul 2024 18:53:27 +0200] rev 81068
vscode: adjusted setting description;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:23:00 +0200] rev 81067
lsp: added support for code actions to apply active sendback markups;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:22:50 +0200] rev 81066
lsp: clarified WorkspaceEdit;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:22:36 +0200] rev 81065
lsp: made TextDocumentEdit accept optional versions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:51 +0200] rev 81064
lsp: tuned;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:45 +0200] rev 81063
lsp: removed code that is never run;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:39 +0200] rev 81062
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:32 +0200] rev 81061
clarified PIDE/line range conversions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:26 +0200] rev 81060
lsp: refactored conversion from Decoration_List to JSON;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:19 +0200] rev 81059
lsp: tuned pretty_text_panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:12 +0200] rev 81058
lsp: removed output_pretty_panel function as its logic is now in pretty_text_panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:31:52 +0200] rev 81057
vscode: added more relevant options;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 14 Jun 2024 10:21:47 +0200] rev 81056
lsp: converted state panel to use a pretty text panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 14 Jun 2024 10:21:28 +0200] rev 81055
lsp: converted dynamic output to use a pretty text panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 14 Jun 2024 10:21:03 +0200] rev 81054
lsp: added Pretty_Text_Panel module;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 21:26:31 +0200] rev 81053
vscode: added relevant isabelle options to vscode settings;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 21:14:41 +0200] rev 81052
vscode: indent;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 21:22:01 +0200] rev 81051
lsp: extracted panel content generation logic;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 20:54:11 +0200] rev 81050
vscode: added all fonts to extension;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 20:44:10 +0200] rev 81049
added vscode options tag;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 30 May 2024 02:43:29 +0200] rev 81048
vscode: tuned;
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;
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;
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;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 16 May 2024 12:00:05 +0200] rev 81037
lsp: added decorations to dynamic output;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 09 May 2024 22:24:19 +0200] rev 81036
lsp: force update after state_set_margin;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 30 May 2024 02:45:01 +0200] rev 81035
vscode: added dynamic and state output set margin messages to vscode extension;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:29:44 +0200] rev 81034
lsp: made margins synchronized;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 03 May 2024 20:13:48 +0200] rev 81033
lsp: added separation for non-html output and state;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 03 May 2024 20:11:41 +0200] rev 81032
lsp: tuned;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 03 May 2024 11:10:58 +0200] rev 81031
lsp: clarified preview_request;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 09 May 2024 23:05:10 +0200] rev 81030
lsp: added Symbols_Request;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 09 May 2024 22:22:44 +0200] rev 81029
lsp: added Output_Set_Margin and State_Set_Margin Notifications;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 01 Jul 2024 18:48:26 +0200] rev 81028
lsp: changed State_Init notification into a request and removed State_Init_Response;