| Wed, 12 Feb 2025 00:40:57 +0100 |
wenzelm |
removed unused imports;
|
file |
diff |
annotate
|
| Sun, 09 Feb 2025 16:24:20 +0100 |
wenzelm |
tuned GUI: no scroll_bottom for completely different output;
|
file |
diff |
annotate
|
| Sun, 09 Feb 2025 16:16:26 +0100 |
wenzelm |
tuned GUI: preserve horizontal scrollbar position;
|
file |
diff |
annotate
|
| 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
|