src/Tools/jEdit/src/rendering.scala
2016-06-22 ago report class parameters within instantiation;
2016-06-21 ago clarified rendering (amending ae9330fdbc16);
2016-06-21 ago position information for literal facts;
2016-06-06 ago added action "isabelle.select-entity";
2016-06-06 ago tuned;
2016-06-06 ago clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
2016-04-15 ago clarified rendering wrt. hyperlinks;
2016-04-15 ago clarified focus visibility;
2016-04-15 ago tuned rendering;
2016-04-14 ago background color for entity def/ref focus;
2016-04-01 ago more markup;
2016-03-30 ago more language markup;
2015-12-19 ago more explicit Pretty.Tree, like in ML;
2015-11-21 ago reverted 2abbe7d700e9: "state" output is not necessarily proof state;
2015-11-21 ago avoid flashing of main text area (visual "grey-out") due to spurious edits, e.g. State panel auto-update;
2015-11-21 ago less intrusive rendering, notably for State dockable;
2015-11-21 ago clarified rendering of Markup.DOC: like Markup.PATH / Markup.URL;
2015-11-13 ago added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-09 ago suppress already persistent state output as well;
2015-11-07 ago syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML;
2015-11-07 ago less confusing markup;
2015-11-07 ago ML cartouches via control antiquotation;
2015-11-05 ago symbolic syntax "\<comment> text";
2015-10-15 ago more markup;
2015-10-15 ago report Markdown document structure;
2015-09-19 ago eliminated pointless jedit_text_overview_limit;
2015-09-14 ago avoid hardwired colors;
2015-08-24 ago more explicit debugger caret rendering;
2015-08-12 ago clarified breakpoint rendering;
2015-08-11 ago support hyperlinks with optional focus change;
2015-08-10 ago tuned signature;
2015-08-10 ago set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
2015-08-10 ago added action to toggle breakpoints (on editor side);
2015-08-10 ago rendering for debugger/breakpoint active state;
2015-08-10 ago tuned signature;
2015-05-03 ago misc tuning, based on warnings by IntelliJ IDEA;
2015-01-08 ago tuned;
2014-12-30 ago explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-23 ago explicit message channels for "state", "information";
2014-12-10 ago more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
2014-12-10 ago more explicit markup for improper commands;
2014-12-09 ago clarified language context, e.g. relevant for symbol completion within cartouches;
2014-12-08 ago expand ML cartouches to Input.source;
2014-12-03 ago clarified token kind;
2014-11-05 ago clarified representation of type Keywords;
2014-11-05 ago explicit type Keyword.Keywords;
2014-10-06 ago completion for bibtex entries;
2014-10-05 ago citation tooltip/hyperlink based on open buffers with .bib files;
2014-09-26 ago support for sub-expression markup;
2014-08-27 ago more explicit Method.modifier with reported position;
2014-08-13 ago tuned;
2014-08-12 ago allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
2014-07-26 ago output state first -- avoid fluctuation wrt. warnings, errors, etc.;
2014-07-21 ago removed unused markup (cf. 2f7d91242b99);
2014-07-21 ago regular message to refer to Simplifier Trace panel (unused);
2014-05-16 ago proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
2014-05-06 ago common support for search field, which is actually a light-weight Highlighter;
2014-05-03 ago support for path completion based on file-system content;
2014-04-26 ago tuned signature;
2014-04-16 ago more specific support for sequence of words;