2015-08-10 wenzelm 2015-08-10 tuned signature;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-01-08 wenzelm 2015-01-08 tuned;
2014-12-30 wenzelm 2014-12-30 explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-12-10 wenzelm 2014-12-10 more informative gutter content: fall-back on background color, e.g. when line numbers are enabled; non-transparent information_message_color like other message colors; removed unused error1_color;
2014-12-10 wenzelm 2014-12-10 more explicit markup for improper commands; clarified CSS rendering;
2014-12-09 wenzelm 2014-12-09 clarified language context, e.g. relevant for symbol completion within cartouches;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-12-03 wenzelm 2014-12-03 clarified token kind;
2014-11-05 wenzelm 2014-11-05 clarified representation of type Keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-10-06 wenzelm 2014-10-06 completion for bibtex entries;
2014-10-05 wenzelm 2014-10-05 citation tooltip/hyperlink based on open buffers with .bib files;
2014-09-26 wenzelm 2014-09-26 support for sub-expression markup;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-13 wenzelm 2014-08-13 tuned;
2014-08-12 wenzelm 2014-08-12 allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
2014-07-26 wenzelm 2014-07-26 output state first -- avoid fluctuation wrt. warnings, errors, etc.;
2014-07-21 wenzelm 2014-07-21 removed unused markup (cf. 2f7d91242b99);
2014-07-21 wenzelm 2014-07-21 regular message to refer to Simplifier Trace panel (unused);
2014-05-16 wenzelm 2014-05-16 proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
2014-05-06 wenzelm 2014-05-06 common support for search field, which is actually a light-weight Highlighter;
2014-05-03 wenzelm 2014-05-03 support for path completion based on file-system content;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-16 wenzelm 2014-04-16 more specific support for sequence of words;
2014-04-16 wenzelm 2014-04-16 tuned signature -- separate module Word;
2014-04-13 wenzelm 2014-04-13 added spell-checker completion dialog, without counting frequency of items due to empty name; tuned signature;
2014-04-12 wenzelm 2014-04-12 more general spell_checker_elements;
2014-04-12 wenzelm 2014-04-12 added spell-checker options; support for rendering bad words;
2014-04-12 wenzelm 2014-04-12 markup for prose words within formal comments;
2014-04-09 wenzelm 2014-04-09 more explicit message discrimination;
2014-04-07 wenzelm 2014-04-07 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
2014-04-03 wenzelm 2014-04-03 more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned;
2014-04-02 wenzelm 2014-04-02 more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;
2014-04-02 wenzelm 2014-04-02 persistent protocol_status, to improve performance of node_status a little;
2014-04-01 wenzelm 2014-04-01 more direct command states -- merge_results is hardly ever needed;
2014-04-01 wenzelm 2014-04-01 more frugal command_status, which is often used in a tight loop;
2014-03-27 wenzelm 2014-03-27 more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;
2014-03-26 wenzelm 2014-03-26 tuned signature -- expose less intermediate information;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 more markup for improper elements;
2014-03-17 wenzelm 2014-03-17 tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
2014-03-17 wenzelm 2014-03-17 tuned signature;
2014-03-14 wenzelm 2014-03-14 discontinued somewhat pointless "thy_script" keyword kind;
2014-03-13 wenzelm 2014-03-13 clarified Path.smart_implode; more informative report and rendering;
2014-03-12 wenzelm 2014-03-12 clarified Markup.operator vs. Markup.delimiter; tuned color;
2014-03-12 wenzelm 2014-03-12 more explicit markup for Token.Literal; Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well; Markup.operator for name of Args.syntax, to override outer keywords like "where"; tuned signature;
2014-03-07 wenzelm 2014-03-07 more detailed description of completion items;
2014-03-05 wenzelm 2014-03-05 more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
2014-03-05 wenzelm 2014-03-05 clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
2014-03-03 wenzelm 2014-03-03 recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
2014-03-03 wenzelm 2014-03-03 clarified path checks: avoid crash of rendering due to spurious errors;
2014-03-03 wenzelm 2014-03-03 more precise navigation within open files;
2014-03-03 wenzelm 2014-03-03 tuned signature;
2014-03-03 wenzelm 2014-03-03 tuned signature;
2014-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;