src/Pure/PIDE/protocol.scala
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);
2014-04-08 ago avoid data redundancy;
2014-04-08 ago tuned signature -- moved Command.Chunk to Text.Chunk;
2014-04-08 ago more explicit Command.Chunk types, less ooddities;
2014-04-07 ago simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
2014-04-07 ago support for URL as file name, similar to treatment in jEdit.java;
2014-04-07 ago separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-04-03 ago more direct warning within persistent Protocol.Status;
2014-04-03 ago more general prover operations;
2014-04-02 ago more explicit iterator terminology, in accordance to Scala 2.8 library;
2014-04-02 ago persistent protocol_status, to improve performance of node_status a little;
2014-04-01 ago tuned for-comprehensions -- less structure mapping;
2014-04-01 ago some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
2014-04-01 ago unused;
2014-04-01 ago more frugal command_status, which is often used in a tight loop;
2014-03-31 ago store blob content within document node: aux. files that were once open are made persistent;
2014-03-27 ago back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
2014-03-27 ago more careful treatment of multiple command states (eval + prints): merge content that is actually required;
2014-03-26 ago clarified valid_id: always standardize towards static command.id;
2014-03-03 ago tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
2014-03-01 ago incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
2014-03-01 ago tuned signature -- more explicit Document.Elements;
2014-02-27 ago more formal Document.Blobs;
2014-02-21 ago tuned signature;
2014-02-18 ago more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
2014-02-12 ago clarified message_positions: cover alt_id as well;
2014-02-11 ago maintain multiple command chunks and markup trees: for main chunk and loaded files;
2014-02-11 ago common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
2014-02-11 ago report (but ignore) markup within auxiliary files;
2013-11-22 ago clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-20 ago load files that are not provided by PIDE blobs;
2013-11-19 ago more explicit indication of missing files;
2013-11-19 ago maintain blobs within document state: digest + text in ML, digest-only in Scala;
2013-11-19 ago clarified boundary cases of Document.Node.Name;
2013-11-18 ago maintain document model for all files, with document view for theory only, and special blob for non-theory files;
2013-08-09 ago cancel_query via direct access to the exec_id of the running query process;
2013-08-05 ago tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-02 ago maintain overlays within node perspective;
2013-07-31 ago allow explicit indication of required node: full eval, no prints;
2013-07-29 ago obsolete;
2013-07-13 ago more rendering for information messages;
2013-07-10 ago tuned signature;
2013-07-09 ago tuned protocol terminology;
2013-07-05 ago tuned signature;
2013-07-05 ago explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 ago separate exec_id assignment for Command.print states, without affecting result of eval;
2013-05-22 ago explicit management of Session.Protocol_Handlers, with protocol state and functions;
2013-05-14 ago tuned signature;
2013-04-29 ago clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
2013-03-26 ago dockable window for timing information;