src/Pure/PIDE/command.scala
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;
2012-09-18 ago some support for inital command markup;
2012-09-14 ago refined output panel: more value-oriented approach to update and caret focus;
2012-08-31 ago more markup for failed goal forks, reusing "bad";
2012-08-24 ago more precise counting of line/column;
2012-08-10 ago clarified undefined, unparsed, unfinished command spans;
2012-08-09 ago tuned signature;
2012-08-07 ago more structural parsing for minor modes;
2012-07-30 ago tuned signature;
2012-04-13 ago include trailing comments in proper_command range;
2012-03-19 ago clarified command span classification: strict Command.is_command, permissive Command.name;
2012-03-13 ago clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-04 ago added Command.proper_range (still unused);
2012-02-27 ago prefer final ADTs -- prevent ooddities;
2012-01-09 ago tuned;
2012-01-07 ago accumulate status as regular markup for command range;
2011-12-01 ago clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
2011-11-29 ago clarified modules;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-26 ago sharing of token source with span source;
2011-11-11 ago prefer statically typed Text.Markup;
2011-09-17 ago Document.Node.Name convenience;
2011-09-01 ago more abstract Document.Node.Name;
2011-08-31 ago maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-25 ago slightly more abstract Command.Perspective;
2011-08-23 ago propagate editor perspective through document model;
2011-08-22 ago some support for editor perspective;
2011-07-09 ago tuned signature;
2011-07-04 ago Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);