src/Pure/PIDE/markup.ML
2016-12-28 ago more uniform treatment of "bad" like other messages (with serial number);
2016-09-05 ago clarified modules;
2016-08-12 ago active jEdit actions;
2016-07-13 ago obsolete;
2016-07-13 ago semantic indentation for unstructured proof scripts;
2016-06-22 ago report class parameters within instantiation;
2016-06-21 ago position information for literal facts;
2016-04-09 ago proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
2016-04-01 ago more markup;
2016-04-01 ago explicit property for unbreakable block;
2016-04-01 ago unused;
2016-04-01 ago clarified treatment of properties;
2016-03-31 ago explicit mixfix block properties;
2016-03-30 ago more language markup;
2016-03-05 ago more PIDE markup;
2016-01-22 ago tuned markup, e.g. relevant for Rendering.tooltip;
2015-12-19 ago support for blocks with consistent breaks;
2015-12-17 ago support pretty break indent, like underlying ML systems;
2015-11-13 ago added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-10 ago added document antiquotation @{theory_text};
2015-11-07 ago clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-07 ago less confusing markup;
2015-11-02 ago clarified completion of Isabelle symbols within document source;
2015-10-15 ago report Markdown document structure;
2015-09-21 ago tuned signature;
2015-08-05 ago protocol support for thread debugger state;
2015-07-30 ago maintain debugger output messages;
2015-07-29 ago separate channel for debugger output;
2015-07-17 ago report possible breakpoint positions;
2015-04-06 ago clarified command keyword markup;
2015-03-24 ago clarified input source;
2015-01-15 ago more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-14 ago clarified build_theories;
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 explicit markup for improper commands;
2014-12-08 ago expand ML cartouches to Input.source;
2014-12-03 ago clarified token kind;
2014-11-11 ago more position information, e.g. relevant for errors in generated ML source;
2014-10-31 ago removed pointless markup;
2014-10-31 ago discontinued obsolete tty and prompt;
2014-10-05 ago citation tooltip/hyperlink based on open buffers with .bib files;
2014-10-05 ago bibtex support in ML: document antiquotation @{cite} with markup;
2014-09-26 ago support for sub-expression markup;
2014-08-27 ago more explicit Method.modifier with reported position;
2014-08-15 ago explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
2014-07-21 ago regular message to refer to Simplifier Trace panel (unused);
2014-05-05 ago support print operations as asynchronous query;
2014-04-26 ago tuned signature;
2014-04-25 ago manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
2014-04-19 ago more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
2014-04-17 ago added protocol command "use_theories", with core functionality of batch build;
2014-04-12 ago markup for prose words within formal comments;
2014-04-08 ago more positions and markup;
2014-03-25 ago separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-18 ago more markup for improper elements;
2014-03-10 ago some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-03-10 ago more markup;
2014-03-06 ago reject internal term names outright, and complete consts instead;
2014-03-05 ago more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;