src/Pure/PIDE/document.scala
2017-01-09 wenzelm 2017-01-09 tuned signature;
2017-01-07 wenzelm 2017-01-07 uniform Document.Model.node_edits (without void edits);
2017-01-07 wenzelm 2017-01-07 obsolete;
2017-01-07 wenzelm 2017-01-07 tuned;
2017-01-06 wenzelm 2017-01-06 tuned;
2017-01-05 wenzelm 2017-01-05 misc tuning and clarification;
2017-01-05 wenzelm 2017-01-05 tuned;
2017-01-05 wenzelm 2017-01-05 tuned;
2016-12-28 wenzelm 2016-12-28 clarified modules;
2016-12-28 wenzelm 2016-12-28 clarified signature: explicit Length to avoid implicit mistakes;
2016-12-23 wenzelm 2016-12-23 tuned;
2016-08-02 wenzelm 2016-08-02 tuned signature -- prover-independence is presently theoretical;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-04-20 wenzelm 2016-04-20 reactivated other_id reports (see also db929027e701, 8eda56033203);
2016-04-18 wenzelm 2016-04-18 tuned signature;
2016-03-01 wenzelm 2016-03-01 clarified modules;
2015-09-19 wenzelm 2015-09-19 straight-forward refresh, without special preconditions; eliminated somewhat expensive eq_content;
2015-08-25 wenzelm 2015-08-25 clarified undefined_blobs: already loaded theories are suppressed; enabled jedit_auto_resolve (again): e.g. relevant for debugging when following links through source files;
2015-08-15 wenzelm 2015-08-15 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
2015-08-12 wenzelm 2015-08-12 resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-03-15 wenzelm 2015-03-15 hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
2015-03-14 wenzelm 2015-03-14 clarified positions of theory imports;
2015-01-15 wenzelm 2015-01-15 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
2015-01-08 wenzelm 2015-01-08 tuned;
2014-12-02 wenzelm 2014-12-02 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
2014-08-17 wenzelm 2014-08-17 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
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;