2013-11-17 wenzelm 2013-11-17 explicit indication of thy_load commands;
2013-09-24 wenzelm 2013-09-24 clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer); simplified command padding: always newline, despite lack of indentation;
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 tuned signature;
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-05 wenzelm 2013-07-05 tuned signature -- eliminated pointless type synonym;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-01-06 wenzelm 2013-01-06 export some generally useful operations;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-09-22 wenzelm 2012-09-22 Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
2012-09-18 wenzelm 2012-09-18 some support for inital command markup; tuned signature;
2012-08-21 wenzelm 2012-08-21 more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;
2012-08-10 wenzelm 2012-08-10 apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;
2012-08-10 wenzelm 2012-08-10 clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;
2012-08-09 wenzelm 2012-08-09 refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.; tuned signature;
2012-08-09 wenzelm 2012-08-09 tuned signature;
2012-08-09 wenzelm 2012-08-09 more direct Linear_Set.reverse, swapping orientation of the graph; tuned;
2012-08-07 wenzelm 2012-08-07 more structural parsing for minor modes; tuned signatures;
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-08-07 wenzelm 2012-08-07 tuned signature;
2012-05-24 wenzelm 2012-05-24 reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");
2012-04-06 wenzelm 2012-04-06 discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-03-19 wenzelm 2012-03-19 clarified command span classification: strict Command.is_command, permissive;
2012-03-16 wenzelm 2012-03-16 more abstract heading level;
2012-03-15 wenzelm 2012-03-15 more explicit header_edits before main text_edits; handle reparses caused by syntax update;
2012-03-15 wenzelm 2012-03-15 basic support for outer syntax keywords in theory header;
2012-03-15 wenzelm 2012-03-15 maintain Version.syntax within document state; clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;
2012-03-04 wenzelm 2012-03-04 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;
2012-03-01 wenzelm 2012-03-01 proper update_header;
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.Version; tuned (NB: Version.nodes is total);
2012-02-26 wenzelm 2012-02-26 more abstract class Document.Node;
2011-11-26 wenzelm 2011-11-26 sharing of token source with span source;
2011-09-01 wenzelm 2011-09-01 more abstract Document.Node.Name; tuned signature;
2011-08-31 wenzelm 2011-08-31 maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Command.Perspective;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Text.Perspective;
2011-08-24 wenzelm 2011-08-24 clarified Document.Node.clear -- retain header (cf. ML version);
2011-08-24 wenzelm 2011-08-24 update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;
2011-08-23 wenzelm 2011-08-23 tuned signature;
2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-13 wenzelm 2011-08-13 maintain node header; misc tuning and clarification;
2011-08-12 wenzelm 2011-08-12 clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-08-11 wenzelm 2011-08-11 explicit datatypes for document node edits;
2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-09 wenzelm 2011-07-09 some support for blobs (arbitrary text files) within document nodes;
2011-07-07 wenzelm 2011-07-07 explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;
2011-07-04 wenzelm 2011-07-04 Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-07-04 wenzelm 2011-07-04 explicit class Counter;
2011-07-03 wenzelm 2011-07-03 tuned signature;
2010-11-28 wenzelm 2010-11-28 tuned signature;
2010-11-11 wenzelm 2010-11-11 unified type Document.Edit;
2010-11-11 wenzelm 2010-11-11 replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character); tuned;
2010-11-10 wenzelm 2010-11-10 proper treatment of equal heading level;
2010-11-10 wenzelm 2010-11-10 some support for nested source structure, based on section headings;