| Wed, 12 Feb 2025 00:40:57 +0100 |
wenzelm |
removed unused imports;
|
file |
diff |
annotate
|
| Thu, 14 Nov 2024 10:50:49 +0100 |
wenzelm |
more careful isConsumed() / consume() for key and mouse events;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2022 22:41:47 +0100 |
wenzelm |
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2022 22:38:03 +0100 |
wenzelm |
clarified signature: proper scopes and types;
|
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
|
| Mon, 06 Apr 2020 12:53:45 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 23 May 2017 13:47:31 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 12 Jan 2017 12:29:12 +0100 |
wenzelm |
more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2016 17:35:12 +0200 |
wenzelm |
make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;
|
file |
diff |
annotate
|
| Thu, 04 Feb 2016 21:22:53 +0100 |
wenzelm |
separate delay_repaint to ensure reactivity, indepently of future_refresh status;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:50:09 +0100 |
wenzelm |
more thorough GUI update;
|
file |
diff |
annotate
|
| Tue, 22 Dec 2015 14:26:35 +0100 |
wenzelm |
more thorough event propagation;
|
file |
diff |
annotate
|
| Tue, 24 Nov 2015 23:17:03 +0100 |
wenzelm |
more scalable GUI;
|
file |
diff |
annotate
|
| Sat, 21 Nov 2015 16:35:46 +0100 |
wenzelm |
render snapshot.is_outdated in text overview, where other status information is shown already;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 16:49:44 +0100 |
wenzelm |
prefer Isabelle/Scala Future;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 13:54:34 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 21:07:37 +0200 |
wenzelm |
straight-forward refresh, without special preconditions;
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 20:47:11 +0200 |
wenzelm |
eliminated pointless jedit_text_overview_limit;
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 20:38:28 +0200 |
wenzelm |
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:22:56 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2014 23:49:15 +0200 |
wenzelm |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 11:49:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 16:10:46 +0100 |
wenzelm |
structural equality for Command.Results;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 23:08:40 +0100 |
wenzelm |
more prominent status ticks;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 14:46:22 +0100 |
wenzelm |
more precise relevant_range to exploit overview_limit better;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 16:27:55 +0200 |
wenzelm |
further attempts to cope with large files via option jedit_text_overview_limit;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 11:39:24 +0200 |
wenzelm |
option to bypass potentially slow text overview;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 20:34:19 +0200 |
wenzelm |
renamed Text_Area_Painter to Rich_Text_Area;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 20:23:25 +0200 |
wenzelm |
tuned signature -- more general Text_Area_Painter operations;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:49:11 +0200 |
wenzelm |
somewhat more general JEdit_Lib;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 13:52:16 +0200 |
wenzelm |
more static handling of rendering options;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:46:33 +0200 |
wenzelm |
tuned options (again);
|
file |
diff |
annotate
|
| Thu, 13 Sep 2012 16:01:42 +0200 |
wenzelm |
more efficient painting based on cached result;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 23:08:27 +0100 |
wenzelm |
explicit propagation of assignment event, even if changed command set is empty;
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 16:04:58 +0100 |
wenzelm |
separate module for text status overview;
|
file |
diff |
annotate
|