2015-04-04 ago more general notion of command span: command keyword not necessarily at start;
2015-03-17 ago misc tuning and simplification;
2015-03-16 ago avoid duplicate header errors, more precise positions;
2015-03-16 ago clarified modules;
2015-03-15 ago more markup, which helps to create missing imports;
2015-03-15 ago proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-15 ago clarified span position;
2015-03-15 ago hybrid use of command blobs: inlined errors and auxiliary files;
2015-03-15 ago tuned;
2015-03-14 ago value-oriented user error, for well-defined Thy_Syntax.chop_common;
2015-03-13 ago simplified Command.resolve_files in ML, using blobs_index from Scala;
2015-03-12 ago clarified command content;
2014-12-30 ago explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-01 ago tuned signature;
2014-08-12 ago tuned;
2014-08-12 ago clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12 ago maintain Command_Range position as in ML;
2014-08-12 ago separate module Command_Span: mostly syntactic representation;
2014-08-11 ago tuned signature;
2014-08-11 ago tuned output, in accordance to transaction name in ML;
2014-08-11 ago more explicit type Span in Scala, according to ML version;
2014-08-02 ago more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
2014-07-23 ago more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-04-29 ago more systematic Isabelle output, like in classic Isabelle/ML (without markup);
2014-04-26 ago tuned signature;
2014-04-26 ago tuned signature;
2014-04-10 ago ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
2014-04-09 ago tuned;
2014-04-08 ago expose more bad cases;
2014-04-08 ago tuned signature;
2014-04-08 ago simplified Text.Chunk -- eliminated ooddities;
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 uniform Command.Chunk operations;
2014-04-08 ago more explicit Command.Chunk types, less ooddities;
2014-04-03 ago more direct warning within persistent Protocol.Status;
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;
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;