| Wed, 11 Dec 2024 12:03:01 +0100 |
wenzelm |
more robust: avoid spurious crash of text_area.getText() in Active_Area.update();
|
file |
diff |
annotate
|
| Sun, 17 Nov 2024 19:49:25 +0100 |
wenzelm |
more operations, to support search within output panel;
|
file |
diff |
annotate
|
| Sun, 17 Nov 2024 13:57:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 16 Nov 2024 19:54:30 +0100 |
wenzelm |
minor performance tuning: avoided repeated metric initialization;
|
file |
diff |
annotate
|
| Sat, 16 Nov 2024 19:07:24 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Fri, 15 Nov 2024 16:50:44 +0100 |
wenzelm |
tuned comments;
|
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
|
| Thu, 14 Nov 2024 11:12:11 +0100 |
wenzelm |
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
|
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
|
| Sun, 10 Nov 2024 16:04:56 +0100 |
wenzelm |
performance tuning: more incremental update of buffer content;
|
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:15:31 +0100 |
wenzelm |
clarified margin operations (again, reverting 4794576828df);
|
file |
diff |
annotate
|
| Sat, 09 Nov 2024 16:34:14 +0100 |
wenzelm |
clarified signature: include standard margin in object equality;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 13:55:54 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2024 20:55:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 01 Nov 2024 15:40:31 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2024 15:51:19 +0200 |
wenzelm |
clarified signature: more arguments;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2024 11:13:21 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 19:00:00 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2022 09:03:06 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 25 Jul 2022 14:40:45 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 15 Jul 2021 16:35:45 +0200 |
wenzelm |
build.props for isabelle.jar, including isabelle.jedit;
|
file |
diff |
annotate
|
| Sat, 08 May 2021 13:06:30 +0200 |
wenzelm |
separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2021 21:37:20 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 21 Dec 2020 21:56:20 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2020 22:01:54 +0100 |
wenzelm |
clarified caret focus modifier, depending on option "jedit_focus_modifier";
|
file |
diff |
annotate
|
| Sun, 13 Dec 2020 16:00:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 22 May 2020 11:30:06 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2020 22:32:10 +0100 |
wenzelm |
proper navigation wrt. caret;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2020 22:05:47 +0100 |
wenzelm |
tuned -- avoid deprecated operations;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2020 21:52:21 +0100 |
wenzelm |
more Isabelle/jEdit actions;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2019 22:35:41 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 23:30:42 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Tue, 01 May 2018 16:42:14 +0200 |
wenzelm |
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
|
file |
diff |
annotate
|
| Mon, 06 Nov 2017 16:03:13 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 15:21:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 15:15:29 +0200 |
wenzelm |
more robust: provide docking framework via base plugin;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2017 20:32:06 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2017 17:28:48 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 11:38:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 19:56:47 +0200 |
wenzelm |
more explicit jEdit file operations;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 20:01:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 23:21:09 +0100 |
wenzelm |
more robust, notably on Windows;
|
file |
diff |
annotate
|
| Sun, 01 Jan 2017 11:47:27 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2016 21:35:56 +0100 |
wenzelm |
clarified module name;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2016 09:47:51 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 22:55:53 +0200 |
wenzelm |
background color for entity def/ref focus;
|
file |
diff |
annotate
|
| Thu, 04 Feb 2016 21:53:06 +0100 |
wenzelm |
re-init document views for the sake of Text_Overview size;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 15:14:59 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 19:34:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 21:08:47 +0200 |
wenzelm |
clarified modules, like ML version;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 19:15:17 +0200 |
wenzelm |
tuned signature, according to ML version;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2015 21:51:34 +0100 |
wenzelm |
updated to jedit-5.2.0;
|
file |
diff |
annotate
|
| Tue, 02 Dec 2014 14:16:56 +0100 |
wenzelm |
node-specific syntax, with base_syntax as default;
|
file |
diff |
annotate
|