src/Pure/PIDE/markup.ML
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;
2014-03-05 ago clarified init_assignable: make double-sure that initial values are reset;
2014-03-02 ago clarified names of antiquotations and markup;
2014-03-01 ago clarified language markup: added "delimited" property;
2014-02-26 ago tuned signature;
2014-02-26 ago method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-25 ago back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
2014-02-25 ago clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
2014-02-23 ago clarified semantic completion: retain kind.full_name as official item name for history;
2014-02-23 ago clarified completion names;
2014-02-22 ago support for completion within the formal context;
2014-02-22 ago refined language context: antiquotes;
2014-02-21 ago more markup -- complete symbols within antiquotation, notably with broken arguments;
2014-02-20 ago completion of keywords and symbols based on language context;
2014-02-19 ago more markup;
2014-02-18 ago more markup;
2014-02-18 ago more standard names for protocol and markup elements;
2014-02-18 ago tuned signature;
2014-02-18 ago generic markup for embedded languages;
2014-02-17 ago more markup;
2014-02-15 ago more uniform ML keyword markup;
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-09-03 ago cases: more position information and PIDE markup;
2013-08-17 ago some protocol to determine provers according to ML;
2013-08-02 ago more general Output.result: allow to update arbitrary properties;
2013-07-30 ago less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
2013-07-18 ago explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-13 ago more explicit Markup.information for messages produced by "auto" tools;
2013-07-09 ago tuned protocol terminology;
2013-05-22 ago explicit management of Session.Protocol_Handlers, with protocol state and functions;
2013-05-14 ago more uniform Markup.print_real;
2013-05-14 ago more uniform Markup.parse_real;
2013-05-12 ago more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
2013-04-09 ago tuned signature;
2013-04-05 ago unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-04-03 ago additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-03-28 ago basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);