src/Pure/PIDE/protocol.scala
2012-12-12 ago support dialog via document content;
2012-12-10 ago generalized notion of active area, where sendback is just one application;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-21 ago tuned whitespace;
2012-11-19 ago alternative completion for outer syntax keywords;
2012-09-28 ago support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28 ago eliminated dead code;
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-08-31 ago clarified command status (again);
2012-08-31 ago further refinement of command status, to accomodate forked proofs;
2012-08-30 ago refined status of forked goals;
2012-08-20 ago added keyword kind "thy_load" (with optional list of file extensions);
2012-08-10 ago apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
2012-08-07 ago simplified Document.Node.Header -- internalized errors;
2012-08-07 ago tuned signature -- slightly more abstract text representation of prover process;
2012-04-18 ago more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
2012-04-07 ago added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-06 ago discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06 ago discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-05 ago less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-03-15 ago some support for outer syntax keyword declarations within theory header;
2012-03-13 ago clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-04 ago clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
2012-03-03 ago retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
2012-03-01 ago Symbol.encode header edits;
2012-02-29 ago clarified module Thy_Load;
2012-02-26 ago include warning messages in node status;
2012-01-15 ago more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
2012-01-14 ago tuned comments;
2012-01-14 ago clarified partial restrict operation;
2012-01-09 ago command status color via regular markup;
2012-01-05 ago prefer raw_message for protocol implementation;
2011-12-01 ago clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;