src/Tools/jEdit/src/graphview_dockable.scala
Sat, 23 Mar 2013 19:39:31 +0100 wenzelm retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
Sun, 17 Mar 2013 21:04:38 +0100 wenzelm 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);
Fri, 14 Dec 2012 12:09:08 +0100 wenzelm more formal class Command.Results;
Thu, 13 Dec 2012 17:29:23 +0100 wenzelm more careful handling of Dialog_Result, with active area and color feedback;
Mon, 10 Dec 2012 15:17:47 +0100 wenzelm stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
Sun, 09 Dec 2012 14:05:21 +0100 wenzelm always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
Sun, 25 Nov 2012 20:59:32 +0100 wenzelm renamed main plugin object to PIDE;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Sun, 25 Nov 2012 18:47:33 +0100 wenzelm quasi-abstract module Rendering, with Isabelle-specific implementation;
Sun, 18 Nov 2012 15:28:58 +0100 wenzelm update options via protocol;
Mon, 08 Oct 2012 20:39:57 +0200 wenzelm more precise repaint and revalidate -- the latter is important to keep in sync with content update;
Mon, 08 Oct 2012 12:40:35 +0200 wenzelm use Pretty_Tooltip for Graphview_Panel;
Wed, 26 Sep 2012 14:38:23 +0200 wenzelm more uniform graphview terminology;
less more (0) tip