src/Tools/jEdit/src/monitor_dockable.scala
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-04-28 wenzelm 2014-04-28 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
2014-04-25 wenzelm 2014-04-25 clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; eliminated old actors;
2014-02-20 wenzelm 2014-02-20 tuned imports;
2013-08-24 wenzelm 2013-08-24 more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
2013-01-18 wenzelm 2013-01-18 use inlined session name as title for charts; tuned signature;
2013-01-03 wenzelm 2013-01-03 more interesting fields;
2013-01-03 wenzelm 2013-01-03 improved Monitor_Dockable, based on ML_Statistics operations; tuned signature;
2012-12-08 wenzelm 2012-12-08 basic monitor panel, using the powerful jfreechart library; sorted Isabelle menu entries -- this is mainly a catalog;