src/Tools/jEdit/src/text_overview.scala
2016-09-02 wenzelm 2016-09-02 make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;
2016-02-04 wenzelm 2016-02-04 separate delay_repaint to ensure reactivity, indepently of future_refresh status; clarified delay_refresh: do not cancel already running task, but retry later;
2016-01-07 wenzelm 2016-01-07 more thorough GUI update;
2015-12-22 wenzelm 2015-12-22 more thorough event propagation;
2015-11-24 wenzelm 2015-11-24 more scalable GUI;
2015-11-21 wenzelm 2015-11-21 render snapshot.is_outdated in text overview, where other status information is shown already;
2015-11-03 wenzelm 2015-11-03 prefer Isabelle/Scala Future;
2015-11-03 wenzelm 2015-11-03 clarified modules;
2015-09-19 wenzelm 2015-09-19 straight-forward refresh, without special preconditions; eliminated somewhat expensive eq_content;
2015-09-19 wenzelm 2015-09-19 eliminated pointless jedit_text_overview_limit;
2015-09-19 wenzelm 2015-09-19 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;
2014-07-23 wenzelm 2014-07-23 tuned comments;
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2013-08-12 wenzelm 2013-08-12 tuned signature;
2013-03-23 wenzelm 2013-03-23 structural equality for Command.Results; more general Command.State.eq_content;
2013-01-14 wenzelm 2013-01-14 more prominent status ticks; is_running takes priority -- important to spot unstable parts that are re-run after edits;
2013-01-14 wenzelm 2013-01-14 more precise relevant_range to exploit overview_limit better;
2012-11-25 wenzelm 2012-11-25 renamed main plugin object to PIDE;
2012-10-22 wenzelm 2012-10-22 further attempts to cope with large files via option jedit_text_overview_limit;
2012-10-04 wenzelm 2012-10-04 option to bypass potentially slow text overview;
2012-09-17 wenzelm 2012-09-17 renamed Text_Area_Painter to Rich_Text_Area;
2012-09-17 wenzelm 2012-09-17 tuned signature -- more general Text_Area_Painter operations;
2012-09-17 wenzelm 2012-09-17 somewhat more general JEdit_Lib; tuned signatures;
2012-09-14 wenzelm 2012-09-14 more static handling of rendering options;
2012-09-14 wenzelm 2012-09-14 tuned options (again);
2012-09-13 wenzelm 2012-09-13 more efficient painting based on cached result;
2012-03-19 wenzelm 2012-03-19 explicit propagation of assignment event, even if changed command set is empty; discontinued slightly odd Document_View.update_snapshot/flush_snapshot;
2012-02-21 wenzelm 2012-02-21 separate module for text status overview;