2014-02-22 ago refined language context: antiquotes;
2014-02-21 ago tuned signature -- avoid redundancy and confusion of flags;
2014-02-21 ago more general / abstract Command.Markups, with separate index for status elements;
2014-02-21 ago more lightweight Rendering;
2014-02-21 ago tuned signature;
2014-02-20 ago tuned comments;
2014-02-20 ago complete symbols within ML strings / comments;
2014-02-20 ago tuned;
2014-02-20 ago clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
2014-02-20 ago cumulate/select wrt. precise elements guard;
2014-02-20 ago tuned;
2014-02-20 ago default completion context via outer syntax;
2014-02-20 ago completion of keywords and symbols based on language context;
2014-02-18 ago generic markup for embedded languages;
2014-02-17 ago hyperlink for visible positions;
2014-02-17 ago more markup;
2014-02-16 ago more uniform rendering of text that is formally interpreted: avoid clash with inner markup;
2014-02-16 ago support ML antiquotations in Scala;
2014-02-15 ago more uniform ML keyword markup;
2014-02-15 ago tuned;
2014-02-15 ago refined ML keyword styles;
2014-02-15 ago isabelle-ml mode with separate token marker;
2014-02-04 ago interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
2014-01-18 ago support for nested text cartouches;
2013-12-09 ago added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-11-19 ago clarified boundary cases of Document.Node.Name;
2013-09-11 ago more explicit indication of 'done' as proof script element;
2013-09-02 ago more explicit indication of 'guess' as improper Isar (aka "script") element;
2013-08-29 ago more abstract Completion_Popup.Text_Area;
2013-08-27 ago determine completion geometry like tooltip;
2013-08-12 ago manage hyperlinks via PIDE editor interface;
2013-08-07 ago more elementary list structures for markup tree traversal;
2013-08-07 ago tuned signature;
2013-08-07 ago more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
2013-08-05 ago tuned signature;
2013-07-13 ago more rendering for information messages;
2013-07-13 ago gutter icon for information messages;
2013-07-13 ago more explicit Markup.information for messages produced by "auto" tools;
2013-07-05 ago explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-06-28 ago load icons via options -- prefer IntelliJ IDEA for now;
2013-06-28 ago support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ IDEA Community Edition 12.1.2);
2013-05-21 ago tuned;
2013-05-21 ago less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
2013-05-20 ago discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-03-30 ago tooltip of command keyword includes timing information;
2013-03-28 ago ghost bullet via markup, which is painted as bar under text (normally space);
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.;