2014-08-02 wenzelm 2014-08-02 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 wenzelm 2014-07-23 more frugal edits;
2014-07-23 wenzelm 2014-07-23 more explicit treatment of cleared nodes (removal is implicit);
2014-07-23 wenzelm 2014-07-23 clarified display;
2014-07-23 wenzelm 2014-07-23 clarified display;
2014-07-23 wenzelm 2014-07-23 avoid redundant data structure;
2014-07-23 wenzelm 2014-07-23 more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-07-23 wenzelm 2014-07-23 tuned;
2014-07-23 wenzelm 2014-07-23 tuned signature;
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-24 wenzelm 2014-04-24 tuned signature;
2014-04-15 wenzelm 2014-04-15 clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
2014-04-10 wenzelm 2014-04-10 ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL; silently ignore excessive reports -- no ambition to detect that situation accurately;
2014-04-09 wenzelm 2014-04-09 tuned;
2014-04-08 wenzelm 2014-04-08 tuned signature;
2014-04-08 wenzelm 2014-04-08 simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway;
2014-04-08 wenzelm 2014-04-08 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
2014-04-08 wenzelm 2014-04-08 tuned signature -- moved Command.Chunk to Text.Chunk;
2014-04-08 wenzelm 2014-04-08 more explicit Command.Chunk types, less ooddities; tuned;
2014-04-04 wenzelm 2014-04-04 afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
2014-04-03 wenzelm 2014-04-03 clarified Version.syntax -- avoid guessing initial situation;
2014-04-03 wenzelm 2014-04-03 more abstract Prover.Syntax, as proposed by Carst Tankink;
2014-04-02 wenzelm 2014-04-02 tuned signature -- more explicit iterator terminology;
2014-04-02 wenzelm 2014-04-02 more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;
2014-04-01 wenzelm 2014-04-01 more direct command states -- merge_results is hardly ever needed;
2014-03-31 wenzelm 2014-03-31 tuned output;
2014-03-31 wenzelm 2014-03-31 tuned signature -- more static typing;
2014-03-31 wenzelm 2014-03-31 store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index;
2014-03-29 wenzelm 2014-03-29 tuned signature;
2014-03-27 wenzelm 2014-03-27 tuned -- avoid code duplication;
2014-03-27 wenzelm 2014-03-27 more frugal merge of markup trees: filter wrt. subsequent query;
2014-03-27 wenzelm 2014-03-27 tuned signature;
2014-03-27 wenzelm 2014-03-27 more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;
2014-03-26 wenzelm 2014-03-26 tuned signature -- expose less intermediate information;
2014-03-26 wenzelm 2014-03-26 clarified valid_id: always standardize towards static;
2014-03-17 wenzelm 2014-03-17 tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
2014-03-01 wenzelm 2014-03-01 tuned signature -- more explicit Document.Elements;
2014-02-28 wenzelm 2014-02-28 tuned data structure;
2014-02-28 wenzelm 2014-02-28 tuned;
2014-02-27 wenzelm 2014-02-27 more formal Document.Blobs; removed junk;
2014-02-27 wenzelm 2014-02-27 tuned output;
2014-02-26 wenzelm 2014-02-26 tuned output;
2014-02-24 wenzelm 2014-02-24 tuned messages;
2014-02-21 wenzelm 2014-02-21 tuned signature -- avoid redundancy and confusion of flags;
2014-02-21 wenzelm 2014-02-21 tuned signature;
2014-02-21 wenzelm 2014-02-21 more general / abstract Command.Markups, with separate index for status elements; slightly faster Rendering.overview_color;
2014-02-20 wenzelm 2014-02-20 cumulate/select wrt. precise elements guard; tuned signature;
2014-02-12 wenzelm 2014-02-12 maintain blob edits within history, which is important for Snapshot.convert/revert;
2014-02-12 wenzelm 2014-02-12 more accurate eq_content;
2014-02-11 wenzelm 2014-02-11 maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;
2014-02-11 wenzelm 2014-02-11 common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content); more informative type Blob, to allow markup reports;
2013-11-22 wenzelm 2013-11-22 clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-21 wenzelm 2013-11-21 actually expose errors of cumulative theory dependencies; more informative error messages;
2013-11-20 wenzelm 2013-11-20 ranges of thy_load commands count as visible within perspective; convert ranges wrt. snapshot -- relevant for outdated situation;
2013-11-20 wenzelm 2013-11-20 refer to thy_load command of auxiliary file;
2013-11-19 wenzelm 2013-11-19 clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;
2013-11-19 wenzelm 2013-11-19 maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
2013-11-19 wenzelm 2013-11-19 clarified boundary cases of Document.Node.Name;