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;
2013-11-18 wenzelm 2013-11-18 inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;
2013-11-18 wenzelm 2013-11-18 tuned;
2013-11-18 wenzelm 2013-11-18 maintain document model for all files, with document view for theory only, and special blob for non-theory files;
2013-11-17 wenzelm 2013-11-17 explicit indication of thy_load commands;
2013-10-12 wenzelm 2013-10-12 more strict find_command -- avoid invalid hyperlink_command;
2013-08-12 wenzelm 2013-08-12 prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;
2013-08-12 wenzelm 2013-08-12 central management of Document.Overlays, independent of Document_Model;
2013-08-12 wenzelm 2013-08-12 tuned -- use Multi_Map;
2013-08-12 wenzelm 2013-08-12 tuned signature;
2013-08-08 wenzelm 2013-08-08 proper low-level comparison -- heed warning by Scala compiler;
2013-08-07 wenzelm 2013-08-07 maintain commands together with index -- avoid redundant reconstruction of full_index;
2013-08-07 wenzelm 2013-08-07 more elementary list structures for markup tree traversal;
2013-08-07 wenzelm 2013-08-07 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
2013-08-07 wenzelm 2013-08-07 tuned signature;
2013-08-05 wenzelm 2013-08-05 tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-05 wenzelm 2013-08-05 commands with overlay remain visible, to avoid loosing printed output;
2013-08-02 wenzelm 2013-08-02 maintain overlays within node perspective; tuned signature;
2013-07-31 wenzelm 2013-07-31 allow explicit indication of required node: full eval, no prints;
2013-07-09 wenzelm 2013-07-09 tuned;
2013-07-09 wenzelm 2013-07-09 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-09 wenzelm 2013-07-09 tuned signature -- NB: is actually part of Command.eval;
2013-07-09 wenzelm 2013-07-09 tuned protocol terminology; tuned signature;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-03-23 wenzelm 2013-03-23 structural equality for Command.Results; more general Command.State.eq_content;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2012-12-13 wenzelm 2012-12-13 identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
2012-11-25 wenzelm 2012-11-25 tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
2012-10-01 wenzelm 2012-10-01 removed unused module Blob;
2012-09-28 wenzelm 2012-09-28 tuned signature;
2012-09-22 wenzelm 2012-09-22 accumulate under exec_id as well;