src/Tools/jEdit/src/monitor_dockable.scala
Thu, 13 Aug 2020 13:13:29 +0200 wenzelm clarified GUI;
Thu, 13 Aug 2020 12:59:41 +0200 wenzelm tuned GUI;
Wed, 12 Aug 2020 11:22:11 +0200 wenzelm removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
Mon, 06 Apr 2020 12:53:45 +0200 wenzelm clarified modules;
Wed, 01 Apr 2020 21:43:22 +0200 wenzelm clarified signature;
Fri, 01 Sep 2017 15:15:29 +0200 wenzelm more robust: provide docking framework via base plugin;
Tue, 27 Jun 2017 21:56:56 +0200 wenzelm clarified defaults;
Tue, 27 Jun 2017 21:36:58 +0200 wenzelm tuned signature;
Wed, 17 May 2017 13:47:19 +0200 wenzelm tuned signature;
Sun, 26 Feb 2017 22:13:07 +0100 wenzelm clarified defaults;
Mon, 05 Sep 2016 22:09:52 +0200 wenzelm clarified modules;
Fri, 27 Nov 2015 18:59:47 +0100 wenzelm more reactive GUI;
Sat, 21 Nov 2015 19:04:39 +0100 wenzelm limit statistics, to avoid exhaustion of heap space or GUI time;
Fri, 06 Nov 2015 18:15:35 +0100 wenzelm tuned;
Wed, 15 Apr 2015 13:55:01 +0200 wenzelm GUI controls for ML_statistics, for more digestible protocol dump;
Fri, 08 Aug 2014 11:43:08 +0200 wenzelm improved monitor panel;
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Mon, 28 Apr 2014 14:41:49 +0200 wenzelm mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
Fri, 25 Apr 2014 12:51:08 +0200 wenzelm clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
Sat, 24 Aug 2013 13:32:51 +0200 wenzelm more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
Fri, 18 Jan 2013 23:33:17 +0100 wenzelm use inlined session name as title for charts;
Thu, 03 Jan 2013 14:10:57 +0100 wenzelm more interesting fields;
Thu, 03 Jan 2013 13:54:45 +0100 wenzelm improved Monitor_Dockable, based on ML_Statistics operations;
Sat, 08 Dec 2012 22:19:24 +0100 wenzelm basic monitor panel, using the powerful jfreechart library;
less more (0) tip