src/Pure/PIDE/protocol.scala
4 months ago ago more scalable on 32-bit Poly/ML;
4 months ago ago more compact representation: approx. factor 2;
11 months ago ago clarified modules;
13 months ago ago less wasteful consolidation, based on PIDE front-end state and recent changes;
13 months ago ago Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
13 months ago ago more node status information;
13 months ago ago tuned signature;
16 months ago ago clarified exported messages, e.g. suppress "information", "tracing";
16 months ago ago tuned;
16 months ago ago support for "use_theories";
17 months ago ago treat sessions as entities with defining position;
18 months ago ago formal treatment of documentation names;
19 months ago ago added document antiquotation @{session name};
21 months ago ago provide theory timing information, similar to command timing but always considered relevant;
21 months ago ago more informative loaded_theories: dependencies and syntax;
21 months ago ago session-qualified theory names are mandatory;
22 months ago ago proper standard_path to revert platform_path in JEdit_Sessions.session_base;
23 months ago ago more explicit failure;
23 months ago ago explicit indication of consolidated nodes;
23 months ago ago maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-04-21 ago eliminated default_qualifier: just a constant;
2017-04-12 ago clarified loaded_theories: map to qualified theory name;
2017-04-12 ago global session_base for PIDE interaction;
2017-04-08 ago more qualifier treatment, but in the end it is still ignored;
2017-04-08 ago tuned signature;
2017-04-04 ago more explicit types;
2017-04-01 ago clarified YXML vs. symbol encoding: operate on whole message;
2017-03-18 ago more realistic PIDE build session;
2016-12-20 ago tuned;
2016-09-05 ago clarified modules;
2016-08-02 ago support 'abbrevs' within theory header;
2016-07-10 ago tuned signature: more uniform Keyword.spec;
2015-10-10 ago more explicit HTML.symbols;
2015-10-09 ago output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-08-20 ago clarified modules, like ML version;
2015-08-10 ago tuned signature;
2015-08-10 ago more thorough Encode.string;
2015-03-17 ago misc tuning and simplification;
2015-03-16 ago tuned protocol -- resolve command positions in ML;
2015-03-16 ago clarified modules;
2015-03-15 ago proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-14 ago clarified positions of theory imports;
2015-03-12 ago clarified markup for embedded files, early before execution;
2015-03-10 ago more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-01-14 ago clarified build_theories;
2015-01-13 ago some support for PIDE batch session;
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-03 ago clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-08-20 ago default command position is only valid for default text chunk (amending dcb758188aa6);
2014-08-12 ago generic process wrapping in Prover;
2014-08-12 ago clarified Position.Identified: do not require range from prover, default to command position;
2014-08-02 ago proper priority for error over warning also for node_status (see 9c5220e05e04);
2014-04-30 ago some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-26 ago tuned signature;
2014-04-26 ago tuned signature;
2014-04-17 ago added protocol command "use_theories", with core functionality of batch build;
2014-04-09 ago more explicit message discrimination;
2014-04-08 ago more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
2014-04-08 ago accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);