| Sun, 30 Jun 2024 15:32:51 +0200 |
Thomas Lindae |
lsp: tuned;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:45 +0200 |
Thomas Lindae |
lsp: removed code that is never run;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:39 +0200 |
Thomas Lindae |
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:32 +0200 |
Thomas Lindae |
clarified PIDE/line range conversions;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:26 +0200 |
Thomas Lindae |
lsp: refactored conversion from Decoration_List to JSON;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:19 +0200 |
Thomas Lindae |
lsp: tuned pretty_text_panel;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:12 +0200 |
Thomas Lindae |
lsp: removed output_pretty_panel function as its logic is now in pretty_text_panel;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:31:52 +0200 |
Thomas Lindae |
vscode: added more relevant options;
|
changeset |
files
|
| Fri, 14 Jun 2024 10:21:47 +0200 |
Thomas Lindae |
lsp: converted state panel to use a pretty text panel;
|
changeset |
files
|
| Fri, 14 Jun 2024 10:21:28 +0200 |
Thomas Lindae |
lsp: converted dynamic output to use a pretty text panel;
|
changeset |
files
|
| Fri, 14 Jun 2024 10:21:03 +0200 |
Thomas Lindae |
lsp: added Pretty_Text_Panel module;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:26:31 +0200 |
Thomas Lindae |
vscode: added relevant isabelle options to vscode settings;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:14:41 +0200 |
Thomas Lindae |
vscode: indent;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:22:01 +0200 |
Thomas Lindae |
lsp: extracted panel content generation logic;
|
changeset |
files
|
| Wed, 12 Jun 2024 20:54:11 +0200 |
Thomas Lindae |
vscode: added all fonts to extension;
|
changeset |
files
|
| Wed, 12 Jun 2024 20:44:10 +0200 |
Thomas Lindae |
added vscode options tag;
|
changeset |
files
|
| Thu, 30 May 2024 02:43:29 +0200 |
Thomas Lindae |
vscode: tuned;
|
changeset |
files
|
| Thu, 30 May 2024 02:43:24 +0200 |
Thomas Lindae |
lsp: refactored non-html dynamic/state output;
|
changeset |
files
|
| Mon, 27 May 2024 13:21:15 +0200 |
Thomas Lindae |
vscode: reduced how often symbol width gets measured;
|
changeset |
files
|
| Mon, 27 May 2024 13:20:31 +0200 |
Thomas Lindae |
vscode: IsabelleDejaVuSansMono for state and output panel;
|
changeset |
files
|
| Mon, 27 May 2024 13:18:29 +0200 |
Thomas Lindae |
vscode: added decoration request on file switch;
|
changeset |
files
|
| Mon, 27 May 2024 13:17:09 +0200 |
Thomas Lindae |
lsp: added decoration_request notification;
|
changeset |
files
|
| Thu, 16 May 2024 11:59:33 +0200 |
Thomas Lindae |
lsp: added decorations to state updates;
|
changeset |
files
|
| Thu, 16 May 2024 11:59:06 +0200 |
Thomas Lindae |
lsp: added delay to dynamic_output updates after a set_margin;
|
changeset |
files
|
| Wed, 15 May 2024 17:04:22 +0200 |
Thomas Lindae |
lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;
|
changeset |
files
|
| Wed, 15 May 2024 16:54:39 +0200 |
Thomas Lindae |
lsp: unified PIDE/decorations and dynamic output decorations format;
|
changeset |
files
|
| Wed, 15 May 2024 00:11:34 +0200 |
Thomas Lindae |
vscode: changed test_string to "mix" to be consistent with jEdit;
|
changeset |
files
|
| Thu, 16 May 2024 12:00:05 +0200 |
Thomas Lindae |
lsp: added decorations to dynamic output;
|
changeset |
files
|
| Thu, 09 May 2024 22:24:19 +0200 |
Thomas Lindae |
lsp: force update after state_set_margin;
|
changeset |
files
|
| Thu, 30 May 2024 02:45:01 +0200 |
Thomas Lindae |
vscode: added dynamic and state output set margin messages to vscode extension;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:29:44 +0200 |
Thomas Lindae |
lsp: made margins synchronized;
|
changeset |
files
|
| Fri, 03 May 2024 20:13:48 +0200 |
Thomas Lindae |
lsp: added separation for non-html output and state;
|
changeset |
files
|
| Fri, 03 May 2024 20:11:41 +0200 |
Thomas Lindae |
lsp: tuned;
|
changeset |
files
|
| Fri, 03 May 2024 11:10:58 +0200 |
Thomas Lindae |
lsp: clarified preview_request;
|
changeset |
files
|
| Thu, 09 May 2024 23:05:10 +0200 |
Thomas Lindae |
lsp: added Symbols_Request;
|
changeset |
files
|
| Thu, 09 May 2024 22:22:44 +0200 |
Thomas Lindae |
lsp: added Output_Set_Margin and State_Set_Margin Notifications;
|
changeset |
files
|
| Mon, 01 Jul 2024 18:48:26 +0200 |
Thomas Lindae |
lsp: changed State_Init notification into a request and removed State_Init_Response;
|
changeset |
files
|
| Wed, 01 May 2024 19:09:26 +0200 |
Thomas Lindae |
lsp: tuned;
|
changeset |
files
|
| Thu, 30 May 2024 02:45:24 +0200 |
Thomas Lindae |
lsp: updated ErrorCodes;
|
changeset |
files
|
| Wed, 01 May 2024 12:34:53 +0200 |
Thomas Lindae |
lsp: added State and Dynamic Output html_output and margin handling;
|
changeset |
files
|
| Wed, 01 May 2024 12:30:53 +0200 |
Thomas Lindae |
lsp: added vscode_html_output option;
|
changeset |
files
|
| Wed, 01 May 2024 11:12:59 +0200 |
Thomas Lindae |
tuned formatting;
|
changeset |
files
|
| Wed, 24 Apr 2024 18:49:43 +0200 |
Thomas Lindae |
lsp: partially revert c0388fbd8096 to get decorations for all keywords;
|
changeset |
files
|
| Wed, 24 Apr 2024 18:48:24 +0200 |
Thomas Lindae |
lsp: added State_Init_Response message;
|
changeset |
files
|
| Thu, 30 May 2024 02:43:16 +0200 |
Thomas Lindae |
lsp: removed change_document normalization because it causes desyncs;
|
changeset |
files
|
| Mon, 30 Sep 2024 20:30:59 +0200 |
wenzelm |
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
|
changeset |
files
|
| Mon, 30 Sep 2024 13:00:42 +0200 |
wenzelm |
less markup: prefer "notatation" over "entity";
|
changeset |
files
|
| Mon, 30 Sep 2024 12:59:50 +0200 |
wenzelm |
clarify comparison of output: ignore token positions, which are somewhat accidental;
|
changeset |
files
|
| Mon, 30 Sep 2024 11:42:52 +0200 |
wenzelm |
clarified order of markup: more uniform input vs. output;
|
changeset |
files
|
| Mon, 30 Sep 2024 10:50:33 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Mon, 30 Sep 2024 10:46:26 +0200 |
wenzelm |
clarified parse tree: always provide root node;
|
changeset |
files
|
| Mon, 30 Sep 2024 10:44:25 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 29 Sep 2024 22:47:14 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:57:47 +0200 |
wenzelm |
clarified markup: avoid conflict of "notation" with "entity", e.g. in "[x,y,z]" without spaces;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:40:37 +0200 |
wenzelm |
more flexible command syntax;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:20:36 +0200 |
wenzelm |
less markup (amending 07ad0b407d38): const = "" is mainly for parentheses syntax -- avoid entity_markup here;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:16:17 +0200 |
wenzelm |
more markup reports: notably "notation=..." within pretty blocks;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:13:17 +0200 |
wenzelm |
more parse tree positions;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:03:28 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 29 Sep 2024 20:11:28 +0200 |
wenzelm |
clarified order for 'print_syntax' command;
|
changeset |
files
|