src/Pure/PIDE/protocol.scala
21 months ago wenzelm 2018-01-19 formal treatment of documentation names;
22 months ago wenzelm 2017-12-16 added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
2017-10-16 wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
2017-09-29 wenzelm 2017-09-29 more informative loaded_theories: dependencies and syntax;
2017-09-28 wenzelm 2017-09-28 session-qualified theory names are mandatory;
2017-09-16 wenzelm 2017-09-16 proper standard_path to revert platform_path in JEdit_Sessions.session_base;
2017-08-14 wenzelm 2017-08-14 more explicit failure;
2017-08-14 wenzelm 2017-08-14 explicit indication of consolidated nodes;
2017-08-08 wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-04-21 wenzelm 2017-04-21 eliminated default_qualifier: just a constant;
2017-04-12 wenzelm 2017-04-12 clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;
2017-04-12 wenzelm 2017-04-12 global session_base for PIDE interaction;
2017-04-08 wenzelm 2017-04-08 more qualifier treatment, but in the end it is still ignored;
2017-04-08 wenzelm 2017-04-08 tuned signature;
2017-04-04 wenzelm 2017-04-04 more explicit types;
2017-04-01 wenzelm 2017-04-01 clarified YXML vs. symbol encoding: operate on whole message; tuned signature;
2017-03-18 wenzelm 2017-03-18 more realistic PIDE build session;
2016-12-20 wenzelm 2016-12-20 tuned;
2016-09-05 wenzelm 2016-09-05 clarified modules;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2015-10-10 wenzelm 2015-10-10 more explicit HTML.symbols; tuned signature;
2015-10-09 wenzelm 2015-10-09 output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-08-20 wenzelm 2015-08-20 clarified modules, like ML version;
2015-08-10 wenzelm 2015-08-10 tuned signature; more rendering;
2015-08-10 wenzelm 2015-08-10 more thorough Encode.string;
2015-03-17 wenzelm 2015-03-17 misc tuning and simplification;
2015-03-16 wenzelm 2015-03-16 tuned protocol -- resolve command positions in ML;
2015-03-16 wenzelm 2015-03-16 clarified modules;
2015-03-15 wenzelm 2015-03-15 proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-14 wenzelm 2015-03-14 clarified positions of theory imports;
2015-03-12 wenzelm 2015-03-12 clarified markup for embedded files, early before execution;
2015-03-10 wenzelm 2015-03-10 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-01-14 wenzelm 2015-01-14 clarified build_theories;
2015-01-13 wenzelm 2015-01-13 some support for PIDE batch session; clarified Thy_Info.use_thys_options and corresponding protocol command;
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 explicit message channels for "state", "information"; separate state_message_color;
2014-12-03 wenzelm 2014-12-03 clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-08-20 wenzelm 2014-08-20 default command position is only valid for default text chunk (amending dcb758188aa6);
2014-08-12 wenzelm 2014-08-12 generic process wrapping in Prover; clarified module arrangement;
2014-08-12 wenzelm 2014-08-12 clarified Position.Identified: do not require range from prover, default to command position;
2014-08-02 wenzelm 2014-08-02 proper priority for error over warning also for node_status (see 9c5220e05e04);
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-17 wenzelm 2014-04-17 added protocol command "use_theories", with core functionality of batch build;
2014-04-09 wenzelm 2014-04-09 more explicit message discrimination;
2014-04-08 wenzelm 2014-04-08 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 wenzelm 2014-04-08 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
2014-04-08 wenzelm 2014-04-08 avoid data redundancy;
2014-04-08 wenzelm 2014-04-08 tuned signature -- moved Command.Chunk to Text.Chunk;
2014-04-08 wenzelm 2014-04-08 more explicit Command.Chunk types, less ooddities; tuned;
2014-04-07 wenzelm 2014-04-07 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
2014-04-07 wenzelm 2014-04-07 support for URL as file name, similar to treatment in jEdit.java;
2014-04-07 wenzelm 2014-04-07 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-04-03 wenzelm 2014-04-03 more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned;
2014-04-03 wenzelm 2014-04-03 more general prover operations;
2014-04-02 wenzelm 2014-04-02 more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;
2014-04-02 wenzelm 2014-04-02 persistent protocol_status, to improve performance of node_status a little;
2014-04-01 wenzelm 2014-04-01 tuned for-comprehensions -- less structure mapping;