2011-08-24 ago update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-22 ago some support for editor perspective;
2011-08-22 ago discontinued redundant Edit_Command_ID;
2011-08-13 ago provide node header via Scala layer;
2011-08-13 ago clarified node header -- exclude master_dir;
2011-08-12 ago simplified class Thy_Header;
2011-08-12 ago clarified Exn.message;
2011-08-11 ago uniform treatment of header edits as document edits;
2011-08-11 ago explicit datatypes for document node edits;
2011-07-12 ago tuned XML modules;
2011-07-11 ago JVM method invocation service via Scala layer;
2011-07-10 ago inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
2011-07-10 ago simplified XML_Data;
2011-07-10 ago less currying in Scala;
2011-07-10 ago propagate header changes to prover process;
2010-11-11 ago unified type Document.Edit;
2010-09-23 ago tuned;
2010-09-23 ago tuned prover message categorization;
2010-09-22 ago Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
2010-09-17 ago some specific message classification;
2010-09-17 ago allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
2010-09-17 ago eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
2010-09-07 ago Document_View: select gutter message icons from markup over line range, not full range results;
2010-09-07 ago basic support for warning/error gutter icons;
2010-09-07 ago Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
2010-09-07 ago Isar_Document.reported_positions: exclude proof state output;
2010-09-02 ago Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
2010-08-31 ago Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
2010-08-22 ago simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
2010-08-20 ago concentrate protocol message formats in Isar_Document;
2010-08-19 ago moved Isar_Document to Pure/PIDE;