src/Tools/jEdit/src/graphview_dockable.scala
2014-07-23 ago clarified module name: facilitate alternative GUI frameworks;
2014-04-22 ago avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2013-09-18 ago tuned signature;
2013-08-28 ago uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-24 ago more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
2013-08-12 ago tuned signature;
2013-07-01 ago avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
2013-07-01 ago clarified tooltip timing of pending event and active state;
2013-06-29 ago more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
2013-06-29 ago tuned signature;
2013-03-23 ago retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-17 ago explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
2012-12-14 ago more formal class Command.Results;
2012-12-13 ago more careful handling of Dialog_Result, with active area and color feedback;
2012-12-10 ago stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
2012-12-09 ago always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
2012-11-25 ago renamed main plugin object to PIDE;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-25 ago quasi-abstract module Rendering, with Isabelle-specific implementation;
2012-11-18 ago update options via protocol;
2012-10-08 ago more precise repaint and revalidate -- the latter is important to keep in sync with content update;
2012-10-08 ago use Pretty_Tooltip for Graphview_Panel;
2012-09-26 ago more uniform graphview terminology;