src/Pure/PIDE/markup.scala
2 months ago wenzelm 2018-09-15 more exports;
3 months ago wenzelm 2018-09-02 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
3 months ago wenzelm 2018-09-01 more explicit status for "canceled" command within theory node;
3 months ago wenzelm 2018-08-27 simplified markup;
3 months ago wenzelm 2018-08-18 optional notification of nodes_status (via progress); more accurate changed.nodes wrt. dep_theories; tuned signature;
6 months ago wenzelm 2018-05-29 more node status information;
6 months ago wenzelm 2018-05-27 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
7 months ago wenzelm 2018-05-11 more scalable -- avoid huge lines within stdout;
7 months ago wenzelm 2018-05-07 store exports within PIDE command state; Markup.Export.unapply: proper NAME;
7 months ago wenzelm 2018-05-06 tuned signature; clarified modules;
7 months ago wenzelm 2018-05-05 protocol message for export of theory resources;
9 months ago wenzelm 2018-03-15 clarified server log; tuned options;
9 months ago wenzelm 2018-03-12 explicit Server.Context with output channels (concurrent write); support for Logger and Progress;
11 months ago wenzelm 2018-01-03 HTML output for Markdown elements; clarified HTML operations;
11 months ago wenzelm 2018-01-02 PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
11 months ago wenzelm 2018-01-02 clarified terminology of "markdown_bullet";
13 months ago wenzelm 2017-10-30 proper order of initialization (amending 9953ae603a23);
14 months ago wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
14 months ago wenzelm 2017-10-16 tuned;
16 months ago wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
18 months ago wenzelm 2017-06-08 more HTML rendering as in Isabelle/jEdit; tuned;
18 months ago wenzelm 2017-05-26 store errors in build_history logs and database;
19 months ago wenzelm 2017-05-07 more operations; tuned;
21 months ago wenzelm 2017-03-20 support to encode/decode command state; support to merge full contents of command state;
21 months ago wenzelm 2017-03-18 more informative session result;
21 months ago wenzelm 2017-03-18 more realistic PIDE build session;
21 months ago wenzelm 2017-03-10 suppress irrelevant markup for VSCode;
2016-10-24 wenzelm 2016-10-24 discontinued unused / untested distinction of separate PIDE modules;
2016-10-23 wenzelm 2016-10-23 more operations (see also properties.ML);
2016-08-12 wenzelm 2016-08-12 active jEdit actions;
2016-07-13 wenzelm 2016-07-13 obsolete;
2016-07-13 wenzelm 2016-07-13 semantic indentation for unstructured proof scripts;
2016-06-22 wenzelm 2016-06-22 report class parameters within instantiation;
2016-06-21 wenzelm 2016-06-21 position information for literal facts; Markup.entry may have empty kind/name;
2016-04-14 wenzelm 2016-04-14 background color for entity def/ref focus;
2016-04-01 wenzelm 2016-04-01 more markup;
2015-12-19 wenzelm 2015-12-19 support for blocks with consistent breaks; tuned;
2015-12-17 wenzelm 2015-12-17 support pretty break indent, like underlying ML systems;
2015-11-13 wenzelm 2015-11-13 added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-07 wenzelm 2015-11-07 less confusing markup;
2015-10-15 wenzelm 2015-10-15 report Markdown document structure;
2015-08-10 wenzelm 2015-08-10 tuned signature; more rendering;
2015-08-05 wenzelm 2015-08-05 protocol support for thread debugger state;
2015-07-30 wenzelm 2015-07-30 maintain debugger output messages;
2015-07-29 wenzelm 2015-07-29 tuned;
2015-07-29 wenzelm 2015-07-29 separate channel for debugger output; clarified thread name;
2015-07-17 wenzelm 2015-07-17 report possible breakpoint positions;
2015-03-15 wenzelm 2015-03-15 tuned signature;
2015-01-15 wenzelm 2015-01-15 more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-14 wenzelm 2015-01-14 more type-safe handler interface; proper progress for Build.Handler;
2015-01-14 wenzelm 2015-01-14 clarified build_theories: proper protocol handler;
2015-01-14 wenzelm 2015-01-14 clarified build_theories;
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 unused;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
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-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete control command category;
2014-10-05 wenzelm 2014-10-05 citation tooltip/hyperlink based on open buffers with .bib files;