Wed, 02 Oct 2024 13:51:45 +0200 updated vscode_extension;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 13:51:45 +0200] rev 81087
updated vscode_extension;
Wed, 02 Oct 2024 13:50:01 +0200 NEWS and CONTRIBUTORS;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 13:50:01 +0200] rev 81086
NEWS and CONTRIBUTORS;
Wed, 02 Oct 2024 10:51:11 +0200 clarified: add operation;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 10:51:11 +0200] rev 81085
clarified: add operation;
Wed, 02 Oct 2024 10:39:32 +0200 minor tuning;
Fabian Huch <huch@in.tum.de> [Wed, 02 Oct 2024 10:39:32 +0200] rev 81084
minor tuning;
Fri, 19 Jul 2024 17:08:20 +0200 lsp: added additional commit characters to immediate completions;
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;
Thu, 18 Jul 2024 23:02:49 +0200 vscode: further adjusted default settings and wordPattern for consistent completion popups;
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;
Thu, 18 Jul 2024 17:59:50 +0200 lsp: added more triggerCharacters to make completion popups more consistent;
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;
Thu, 18 Jul 2024 01:18:43 +0200 vscode: added default setting to make completions pop up by themselves;
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;
Thu, 18 Jul 2024 22:08:46 +0200 lsp: improved completions;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 18 Jul 2024 22:08:46 +0200] rev 81079
lsp: improved completions;
Wed, 17 Jul 2024 21:03:56 +0200 vscode: removed unused code;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 17 Jul 2024 21:03:56 +0200] rev 81078
vscode: removed unused code;
Wed, 17 Jul 2024 21:02:30 +0200 vscode: removed README because its content is outdated;
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;
Wed, 17 Jul 2024 20:56:27 +0200 vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;
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;
Tue, 09 Jul 2024 16:47:48 +0200 lsp: added symbol conversion request;
Thomas Lindae <thomas.lindae@in.tum.de> [Tue, 09 Jul 2024 16:47:48 +0200] rev 81075
lsp: added symbol conversion request;
Fri, 05 Jul 2024 21:40:39 +0200 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 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;
Fri, 05 Jul 2024 13:30:07 +0200 vscode: removed unused import;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 05 Jul 2024 13:30:07 +0200] rev 81073
vscode: removed unused import;
Fri, 05 Jul 2024 13:16:47 +0200 vscode: changed vscode_unicode_symbols_edits option default to true;
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;
Fri, 05 Jul 2024 13:15:50 +0200 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:50 +0200] rev 81071
vscode: made uri equality check on actual strings, not on the functions;
Fri, 05 Jul 2024 13:15:05 +0200 vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
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;
Mon, 01 Jul 2024 04:34:04 +0200 lsp: added rudimentary indenting to code actions;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 01 Jul 2024 04:34:04 +0200] rev 81069
lsp: added rudimentary indenting to code actions;
Mon, 01 Jul 2024 18:53:27 +0200 vscode: adjusted setting description;
Thomas Lindae <thomas.lindae@in.tum.de> [Mon, 01 Jul 2024 18:53:27 +0200] rev 81068
vscode: adjusted setting description;
Sun, 30 Jun 2024 15:23:00 +0200 lsp: added support for code actions to apply active sendback markups;
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;
Sun, 30 Jun 2024 15:22:50 +0200 lsp: clarified WorkspaceEdit;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:22:50 +0200] rev 81066
lsp: clarified WorkspaceEdit;
Sun, 30 Jun 2024 15:22:36 +0200 lsp: made TextDocumentEdit accept optional versions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:22:36 +0200] rev 81065
lsp: made TextDocumentEdit accept optional versions;
Sun, 30 Jun 2024 15:32:51 +0200 lsp: tuned;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:51 +0200] rev 81064
lsp: tuned;
Sun, 30 Jun 2024 15:32:45 +0200 lsp: removed code that is never run;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:45 +0200] rev 81063
lsp: removed code that is never run;
Sun, 30 Jun 2024 15:32:39 +0200 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:39 +0200] rev 81062
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Sun, 30 Jun 2024 15:32:32 +0200 clarified PIDE/line range conversions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:32 +0200] rev 81061
clarified PIDE/line range conversions;
Sun, 30 Jun 2024 15:32:26 +0200 lsp: refactored conversion from Decoration_List to JSON;
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;
Sun, 30 Jun 2024 15:32:19 +0200 lsp: tuned pretty_text_panel;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:19 +0200] rev 81059
lsp: tuned pretty_text_panel;
Sun, 30 Jun 2024 15:32:12 +0200 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:32:12 +0200] rev 81058
lsp: removed output_pretty_panel function as its logic is now in pretty_text_panel;
Sun, 30 Jun 2024 15:31:52 +0200 vscode: added more relevant options;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:31:52 +0200] rev 81057
vscode: added more relevant options;
Fri, 14 Jun 2024 10:21:47 +0200 lsp: converted state panel to use a pretty text panel;
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;
Fri, 14 Jun 2024 10:21:28 +0200 lsp: converted dynamic output 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;
Fri, 14 Jun 2024 10:21:03 +0200 lsp: added Pretty_Text_Panel module;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 14 Jun 2024 10:21:03 +0200] rev 81054
lsp: added Pretty_Text_Panel module;
Wed, 12 Jun 2024 21:26:31 +0200 vscode: added relevant isabelle options to vscode settings;
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;
Wed, 12 Jun 2024 21:14:41 +0200 vscode: indent;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 21:14:41 +0200] rev 81052
vscode: indent;
Wed, 12 Jun 2024 21:22:01 +0200 lsp: extracted panel content generation logic;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 21:22:01 +0200] rev 81051
lsp: extracted panel content generation logic;
Wed, 12 Jun 2024 20:54:11 +0200 vscode: added all fonts to extension;
Thomas Lindae <thomas.lindae@in.tum.de> [Wed, 12 Jun 2024 20:54:11 +0200] rev 81050
vscode: added all fonts to extension;
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;
Thu, 16 May 2024 11:59:06 +0200 lsp: added delay to dynamic_output updates after a set_margin;
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;
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;
Thu, 16 May 2024 12:00:05 +0200 lsp: added decorations to dynamic output;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 16 May 2024 12:00:05 +0200] rev 81037
lsp: added decorations to dynamic output;
Thu, 09 May 2024 22:24:19 +0200 lsp: force update after state_set_margin;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 09 May 2024 22:24:19 +0200] rev 81036
lsp: force update after state_set_margin;
Thu, 30 May 2024 02:45:01 +0200 vscode: added dynamic and state output set margin messages to vscode extension;
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;
Sun, 30 Jun 2024 15:29:44 +0200 lsp: made margins synchronized;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:29:44 +0200] rev 81034
lsp: made margins synchronized;
Fri, 03 May 2024 20:13:48 +0200 lsp: added separation for non-html output and state;
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;
Fri, 03 May 2024 20:11:41 +0200 lsp: tuned;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 03 May 2024 20:11:41 +0200] rev 81032
lsp: tuned;
Fri, 03 May 2024 11:10:58 +0200 lsp: clarified preview_request;
Thomas Lindae <thomas.lindae@in.tum.de> [Fri, 03 May 2024 11:10:58 +0200] rev 81031
lsp: clarified preview_request;
Thu, 09 May 2024 23:05:10 +0200 lsp: added Symbols_Request;
Thomas Lindae <thomas.lindae@in.tum.de> [Thu, 09 May 2024 23:05:10 +0200] rev 81030
lsp: added Symbols_Request;
Thu, 09 May 2024 22:22:44 +0200 lsp: added Output_Set_Margin and State_Set_Margin Notifications;
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;
Mon, 01 Jul 2024 18:48:26 +0200 lsp: changed State_Init notification into a request and removed State_Init_Response;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 tip