2013-05-20 wenzelm 2013-05-20 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-03-30 wenzelm 2013-03-30 tooltip of command keyword includes timing information;
2013-03-28 wenzelm 2013-03-28 ghost bullet via markup, which is painted as bar under text (normally space);
2013-03-23 wenzelm 2013-03-23 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-01-14 wenzelm 2013-01-14 more prominent status ticks; is_running takes priority -- important to spot unstable parts that are re-run after edits;
2013-01-04 wenzelm 2013-01-04 prefer old graph browser in Isabelle/jEdit, which still produces better layout; clarified print mode "active_graph": allow to switch "browser" vs. "graphview" uniformly; tuned signature;
2012-12-30 wenzelm 2012-12-30 tuned rendering;
2012-12-15 wenzelm 2012-12-15 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; more tooltip options via Rendering;
2012-12-15 wenzelm 2012-12-15 tuned;
2012-12-15 wenzelm 2012-12-15 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
2012-12-15 wenzelm 2012-12-15 fold main goal;
2012-12-15 wenzelm 2012-12-15 fold handling within Pretty_Text_Area, based on formal document content, which is static here; fold subgoals;
2012-12-14 wenzelm 2012-12-14 more formal class Command.Results;
2012-12-13 wenzelm 2012-12-13 include command results in tooltip as well;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-12-13 wenzelm 2012-12-13 identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
2012-12-12 wenzelm 2012-12-12 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 wenzelm 2012-12-12 support dialog via document content;
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-26 wenzelm 2012-11-26 more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
2012-11-25 wenzelm 2012-11-25 tuned signature; uniform view.fontsize fallback;
2012-11-25 wenzelm 2012-11-25 renamed main plugin object to PIDE;
2012-11-25 wenzelm 2012-11-25 tuned file name;