src/Pure/PIDE/command.scala
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-03-31 ago store blob content within document node: aux. files that were once open are made persistent;
2014-03-27 ago more frugal merge of markup trees: filter wrt. subsequent query;
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-02-27 ago reparse only for actually changed blobs;
2014-02-26 ago tuned output;
2014-02-21 ago tuned signature;
2014-02-21 ago more general / abstract Command.Markups, with separate index for status elements;
2014-02-21 ago tuned signature -- avoid obscure default arguments;
2014-02-20 ago clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
2014-02-20 ago tuned imports;
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 more accurate eq_content;
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 tuned signature;
2014-02-11 ago report (but ignore) markup within auxiliary files;
2013-11-20 ago ranges of thy_load commands count as visible within perspective;
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 proper Thy_Load.append of auxiliary file names;
2013-11-18 ago inline blobs into command, via SHA1 digest;
2013-11-17 ago explicit indication of thy_load commands;
2013-08-09 ago retain original messages properties, e.g. for retrieval via Command.Results;
2013-08-02 ago maintain overlays within node perspective;
2013-07-13 ago full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
2013-07-05 ago tuned signature;
2013-07-05 ago tuned signature -- eliminated pointless type synonym;
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-07-04 ago tuned;
2013-07-03 ago tuned signature;
2013-07-03 ago tuned signature;
2013-03-23 ago retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 ago structural equality for Command.Results;
2013-01-25 ago clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
2012-12-14 ago tuned;
2012-12-14 ago tuned implementation according to Library.insert/merge in ML;
2012-12-14 ago more formal class Command.Results;
2012-12-13 ago more careful handling of Dialog_Result, with active area and color feedback;
2012-12-13 ago identify dialogs via official serial and maintain as result message;
2012-12-12 ago rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 ago more abstract Sendback operations, with explicit id/exec_id properties;
2012-11-21 ago always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
2012-09-28 ago tuned signature;
2012-09-27 ago operations to turn markup into XML;
2012-09-22 ago accumulate under exec_id as well;
2012-09-22 ago more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
2012-09-21 ago more realistic sendback: pick exec_id from message position and text from buffer;
2012-09-20 ago tuned signature;
2012-09-19 ago earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-18 ago more explicit message markup and rendering;
2012-09-18 ago some actual rich text markup via XML.content_markup;