src/Tools/jEdit/src/rendering.scala
2013-03-23 ago retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-01-14 ago more prominent status ticks;
2013-01-04 ago prefer old graph browser in Isabelle/jEdit, which still produces better layout;
2012-12-30 ago tuned rendering;
2012-12-15 ago more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
2012-12-15 ago tuned;
2012-12-15 ago explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
2012-12-15 ago fold main goal;
2012-12-15 ago fold handling within Pretty_Text_Area, based on formal document content, which is static here;
2012-12-14 ago more formal class Command.Results;
2012-12-13 ago include command results in tooltip as well;
2012-12-13 ago more careful handling of Dialog_Result, with active area and color feedback;
2012-12-13 ago identify dialogs via official serial and maintain as result message;
2012-12-12 ago rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
2012-12-12 ago support dialog via document content;
2012-12-10 ago generalized notion of active area, where sendback is just one application;
2012-11-26 ago more general sendback properties;
2012-11-25 ago tuned signature;
2012-11-25 ago renamed main plugin object to PIDE;
2012-11-25 ago tuned file name;