src/Tools/jEdit/src/text_overview.scala
Mon, 06 Apr 2020 12:53:45 +0200 wenzelm clarified modules;
Tue, 23 May 2017 13:47:31 +0200 wenzelm clarified modules;
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;
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;
Thu, 04 Feb 2016 21:22:53 +0100 wenzelm separate delay_repaint to ensure reactivity, indepently of future_refresh status;
Thu, 07 Jan 2016 15:50:09 +0100 wenzelm more thorough GUI update;
Tue, 22 Dec 2015 14:26:35 +0100 wenzelm more thorough event propagation;
Tue, 24 Nov 2015 23:17:03 +0100 wenzelm more scalable GUI;
Sat, 21 Nov 2015 16:35:46 +0100 wenzelm render snapshot.is_outdated in text overview, where other status information is shown already;
Tue, 03 Nov 2015 16:49:44 +0100 wenzelm prefer Isabelle/Scala Future;
Tue, 03 Nov 2015 13:54:34 +0100 wenzelm clarified modules;
Sat, 19 Sep 2015 21:07:37 +0200 wenzelm straight-forward refresh, without special preconditions;
Sat, 19 Sep 2015 20:47:11 +0200 wenzelm eliminated pointless jedit_text_overview_limit;
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;
Wed, 23 Jul 2014 11:22:56 +0200 wenzelm tuned comments;
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Tue, 22 Apr 2014 23:49:15 +0200 wenzelm avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
Mon, 12 Aug 2013 11:49:58 +0200 wenzelm tuned signature;
Sat, 23 Mar 2013 16:10:46 +0100 wenzelm structural equality for Command.Results;
Mon, 14 Jan 2013 23:08:40 +0100 wenzelm more prominent status ticks;
Mon, 14 Jan 2013 14:46:22 +0100 wenzelm more precise relevant_range to exploit overview_limit better;
Sun, 25 Nov 2012 20:59:32 +0100 wenzelm renamed main plugin object to PIDE;
Mon, 22 Oct 2012 16:27:55 +0200 wenzelm further attempts to cope with large files via option jedit_text_overview_limit;
Thu, 04 Oct 2012 11:39:24 +0200 wenzelm option to bypass potentially slow text overview;
Mon, 17 Sep 2012 20:34:19 +0200 wenzelm renamed Text_Area_Painter to Rich_Text_Area;
Mon, 17 Sep 2012 20:23:25 +0200 wenzelm tuned signature -- more general Text_Area_Painter operations;
Mon, 17 Sep 2012 17:49:11 +0200 wenzelm somewhat more general JEdit_Lib;
Fri, 14 Sep 2012 13:52:16 +0200 wenzelm more static handling of rendering options;
Fri, 14 Sep 2012 12:46:33 +0200 wenzelm tuned options (again);
Thu, 13 Sep 2012 16:01:42 +0200 wenzelm more efficient painting based on cached result;
Mon, 19 Mar 2012 23:08:27 +0100 wenzelm explicit propagation of assignment event, even if changed command set is empty;
Tue, 21 Feb 2012 16:04:58 +0100 wenzelm separate module for text status overview;
less more (0) tip