src/Tools/VSCode/src/dynamic_output.scala
Thu, 30 May 2024 02:43:24 +0200 Thomas Lindae lsp: refactored non-html dynamic/state output;
Thu, 16 May 2024 11:59:06 +0200 Thomas Lindae lsp: added delay to dynamic_output updates after a set_margin;
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;
Wed, 15 May 2024 16:54:39 +0200 Thomas Lindae lsp: unified PIDE/decorations and dynamic output decorations format;
Thu, 16 May 2024 12:00:05 +0200 Thomas Lindae lsp: added decorations to dynamic output;
Sun, 30 Jun 2024 15:29:44 +0200 Thomas Lindae lsp: made margins synchronized;
Fri, 03 May 2024 20:13:48 +0200 Thomas Lindae lsp: added separation for non-html output and state;
Thu, 09 May 2024 22:22:44 +0200 Thomas Lindae lsp: added Output_Set_Margin and State_Set_Margin Notifications;
Wed, 01 May 2024 12:34:53 +0200 Thomas Lindae lsp: added State and Dynamic Output html_output and margin handling;
Fri, 23 Dec 2022 22:41:47 +0100 wenzelm more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
Fri, 26 Aug 2022 11:57:05 +0200 wenzelm clarified signature;
Sun, 21 Aug 2022 11:59:25 +0200 wenzelm clarified modules;
Sat, 20 Aug 2022 17:25:55 +0200 wenzelm clarified modules;
Sat, 20 Aug 2022 17:01:34 +0200 wenzelm clarified names;
Sat, 13 Aug 2022 14:29:59 +0200 wenzelm more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
Wed, 27 Jul 2022 09:03:06 +0200 wenzelm clarified signature;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Fri, 25 Feb 2022 16:54:50 +0100 wenzelm proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
Tue, 22 Feb 2022 11:53:06 +0100 wenzelm various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sat, 28 Nov 2020 20:14:46 +0100 wenzelm avoid conflicting base names;
Tue, 21 Apr 2020 19:07:11 +0200 wenzelm clarified imports;
Wed, 15 Jan 2020 19:54:50 +0100 wenzelm misc tuning, following hint by IntelliJ;
Sat, 01 Jun 2019 21:43:41 +0200 wenzelm tuned imports -- accommodate scala-2.13.0-RC3;
Tue, 13 Jun 2017 22:39:57 +0200 wenzelm clarified signature;
Tue, 30 May 2017 21:38:38 +0200 wenzelm tuned signature;
Tue, 23 May 2017 14:23:26 +0200 wenzelm tuned;
Sun, 12 Mar 2017 17:59:03 +0100 wenzelm clarified current_command: index refers to node content, negative index means first command;
Sun, 12 Mar 2017 14:43:50 +0100 wenzelm clarified caret offset;
Sun, 12 Mar 2017 13:48:10 +0100 wenzelm tuned;
Sun, 12 Mar 2017 13:14:24 +0100 wenzelm misc tuning and simplification;
Sat, 11 Mar 2017 23:12:55 +0100 wenzelm dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
less more (0) tip