| Sun, 09 Feb 2025 12:47:21 +0100 |
wenzelm |
tuned: more robust Isabelle symbols;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2025 11:55:20 +0100 |
wenzelm |
proper GUI.Style_HTML.make_text, e.g. for term "x < y";
|
file |
diff |
annotate
|
| Fri, 27 Dec 2024 16:54:48 +0100 |
wenzelm |
more accurate treatment of plain text (amending eede0cf38a63);
|
file |
diff |
annotate
|
| Wed, 18 Dec 2024 11:59:38 +0100 |
wenzelm |
tuned GUI: more informative search_title;
|
file |
diff |
annotate
|
| Tue, 17 Dec 2024 14:56:13 +0100 |
wenzelm |
tuned GUI: trim text as in org.gjt.sp.jedit.search.HyperSearchResult;
|
file |
diff |
annotate
|
| Sat, 07 Dec 2024 11:13:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Nov 2024 23:07:06 +0100 |
wenzelm |
more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);
|
file |
diff |
annotate
|
| Mon, 18 Nov 2024 16:48:11 +0100 |
wenzelm |
tuned output: formatting is pointless for proportional font;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2024 14:47:17 +0100 |
wenzelm |
more robust update;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2024 12:36:56 +0100 |
wenzelm |
Output_Dockable: show search results as tree view;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2024 11:12:51 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 15 Nov 2024 16:08:56 +0100 |
wenzelm |
clarified key events: cancel output selection, before input selection;
|
file |
diff |
annotate
|
| Fri, 15 Nov 2024 16:01:41 +0100 |
wenzelm |
more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";
|
file |
diff |
annotate
|
| Fri, 15 Nov 2024 13:31:36 +0100 |
wenzelm |
more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);
|
file |
diff |
annotate
|
| Thu, 14 Nov 2024 11:33:51 +0100 |
wenzelm |
disable 2d9b6e32632d for now: unknown problems on macOS;
|
file |
diff |
annotate
|
| Wed, 13 Nov 2024 11:53:02 +0100 |
wenzelm |
more ambitious scrolling: retain original scroll position if possible;
|
file |
diff |
annotate
|
| Wed, 13 Nov 2024 10:56:17 +0100 |
wenzelm |
more ambitious scrolling: retain bottom position after output;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2024 22:30:45 +0100 |
wenzelm |
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2024 11:32:07 +0100 |
wenzelm |
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
|
file |
diff |
annotate
|
| Mon, 11 Nov 2024 12:47:51 +0100 |
wenzelm |
clarified signature and modules;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 14:58:05 +0100 |
wenzelm |
clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 12:56:38 +0100 |
wenzelm |
clarified signature and data storage: incremental lazy values;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 12:23:41 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 12:15:31 +0100 |
wenzelm |
clarified margin operations (again, reverting 4794576828df);
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 11:55:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2024 11:38:23 +0100 |
wenzelm |
more reactive interrupts (via Future.cancel);
|
file |
diff |
annotate
|
| Sat, 09 Nov 2024 21:34:38 +0100 |
wenzelm |
Document.Snapshot: support for multiple snippet_commands;
|
file |
diff |
annotate
|
| Sat, 09 Nov 2024 16:39:33 +0100 |
wenzelm |
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;
|
file |
diff |
annotate
|
| Sat, 09 Nov 2024 16:34:14 +0100 |
wenzelm |
clarified signature: include standard margin in object equality;
|
file |
diff |
annotate
|
| Sat, 09 Nov 2024 16:01:07 +0100 |
wenzelm |
performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 18:34:33 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 15:08:36 +0100 |
wenzelm |
more accurate pretty_margin for proportional fonts;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 14:44:29 +0100 |
wenzelm |
clarified signature: more uniform;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 13:42:25 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 13:27:26 +0100 |
wenzelm |
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 15:42:35 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 13:30:40 +0100 |
wenzelm |
clarified signature: more accurate types;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 13:22:59 +0100 |
wenzelm |
more uniform pretty_text_area.zoom via its zoom_component;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 12:26:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 12:17:18 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 12:08:32 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 07 Nov 2024 11:46:21 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 06 Nov 2024 22:04:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2024 20:55:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2022 22:38:03 +0100 |
wenzelm |
clarified signature: proper scopes and types;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 12:32:38 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 12:06:29 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 11:26:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 11:18:22 +0200 |
wenzelm |
tuned signature, following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 15:14:27 +0100 |
wenzelm |
clarified pretty margin: attempt to avoid scrollbar;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 13:04:29 +0100 |
wenzelm |
more informative errors: simplify diagnosis of spurious failures reported by users;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2020 16:00:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 15:18:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 14:48:22 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 12:53:45 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2020 22:14:11 +0100 |
wenzelm |
clarified modifier: avoid confusion of CS+a as C+a;
|
file |
diff |
annotate
|