src/Pure/PIDE/markup.scala
2 months ago ago markup and document markers for some meta data from "Dublin Core Metadata Element Set";
3 months ago ago added executable flag for exports;
4 months ago ago clarified message;
4 months ago ago support hyperlink to theory exports;
4 months ago ago update theory sources based on PIDE markup;
6 months ago ago more comment markup;
8 months ago ago more exports;
8 months ago ago clarified quasi_consolidated state: ensure that exports are present for ok nodes;
8 months ago ago more explicit status for "canceled" command within theory node;
8 months ago ago simplified markup;
9 months ago ago optional notification of nodes_status (via progress);
11 months ago ago more node status information;
12 months ago ago markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
12 months ago ago more scalable -- avoid huge lines within stdout;
12 months ago ago store exports within PIDE command state;
12 months ago ago tuned signature;
12 months ago ago protocol message for export of theory resources;
14 months ago ago clarified server log;
14 months ago ago explicit Server.Context with output channels (concurrent write);
16 months ago ago HTML output for Markdown elements;
16 months ago ago PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
16 months ago ago clarified terminology of "markdown_bullet";
18 months ago ago proper order of initialization (amending 9953ae603a23);
19 months ago ago provide theory timing information, similar to command timing but always considered relevant;
19 months ago ago tuned;
21 months ago ago maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
23 months ago ago more HTML rendering as in Isabelle/jEdit;
24 months ago ago store errors in build_history logs and database;
2017-05-07 ago more operations;
2017-03-20 ago support to encode/decode command state;
2017-03-18 ago more informative session result;
2017-03-18 ago more realistic PIDE build session;
2017-03-10 ago suppress irrelevant markup for VSCode;
2016-10-24 ago discontinued unused / untested distinction of separate PIDE modules;
2016-10-23 ago more operations (see also properties.ML);
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-14 ago background color for entity def/ref focus;
2016-04-01 ago more markup;
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-07 ago less confusing markup;
2015-10-15 ago report Markdown document structure;
2015-08-10 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 tuned;
2015-07-29 ago separate channel for debugger output;
2015-07-17 ago report possible breakpoint positions;
2015-03-15 ago tuned signature;
2015-01-15 ago more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-14 ago more type-safe handler interface;
2015-01-14 ago clarified build_theories: proper protocol handler;
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 unused;