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;
2014-03-01 wenzelm 2014-03-01 tuned;
2014-03-01 wenzelm 2014-03-01 font size change with delay, to avoid GUI lagging behind user input;
2014-03-01 wenzelm 2014-03-01 tuned signature -- more explicit Document.Elements;
2014-02-27 wenzelm 2014-02-27 simplified rendering -- no need to over-emphasize "token_range";
2014-02-26 wenzelm 2014-02-26 markup for method combinators;
2014-02-25 wenzelm 2014-02-25 tuned signature;
2014-02-25 wenzelm 2014-02-25 more completion rendering: active, semantic, syntactic; tuned;
2014-02-25 wenzelm 2014-02-25 tuned;
2014-02-24 wenzelm 2014-02-24 clarified painting of invisible caret, e.g. focus change due to popup;
2014-02-24 wenzelm 2014-02-24 tuned messages;
2014-02-23 wenzelm 2014-02-23 clarified stretch_point_range wrt. UTF-16 surrogates; tuned;
2014-02-23 wenzelm 2014-02-23 tuned;
2014-02-23 wenzelm 2014-02-23 some rendering of completion range; tuned;
2014-02-23 wenzelm 2014-02-23 clarified completion names; tuned signature;
2014-02-22 wenzelm 2014-02-22 support for semantic completion on Scala side;
2014-02-22 wenzelm 2014-02-22 refined language context: antiquotes; support default completions, with move of caret position; tuned signature;