2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-08-22 wenzelm 2011-08-22 discontinued redundant Edit_Command_ID;
2011-08-16 wenzelm 2011-08-16 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;
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 tuned signature;
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-12 wenzelm 2011-08-12 normalized theory dependencies wrt. file_store;
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-12 wenzelm 2011-08-12 simplified class Thy_Header;
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-12 wenzelm 2011-07-12 more uniform Properties in ML and Scala;
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-06-18 wenzelm 2011-06-18 select_markup: no filtering here -- results may be distorted anyway;
2011-06-17 wenzelm 2011-06-17 more explicit error message; convert/revert range; tuned;
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-09-25 wenzelm 2010-09-25 tuned signature;
2010-09-22 wenzelm 2010-09-22 Snapshot.convert/revert: explicit error report to isolate sporadic crash;
2010-09-07 wenzelm 2010-09-07 concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
2010-09-07 wenzelm 2010-09-07 simplified Stream instead of Iterator (again), explicit Option instead of default; tuned Snapshot.convert/revert;
2010-09-01 wenzelm 2010-09-01 Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;
2010-08-31 wenzelm 2010-08-31 Node.full_index: allow command spans larger than block_size;
2010-08-31 wenzelm 2010-08-31 Document state assignment indicates command change;
2010-08-31 wenzelm 2010-08-31 simplified/clarified Document_View.text_area_extension; tuned Document.Node.block_size, trading some space for better time;
2010-08-31 wenzelm 2010-08-31 Document.Node: significant speedup of command_range etc. via lazy full_index;
2010-08-30 wenzelm 2010-08-30 Command.results: ordered by serial number;
2010-08-29 wenzelm 2010-08-29 use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled; clarified session signalling;
2010-08-29 wenzelm 2010-08-29 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; plain Iterator; misc tuning and simplification;
2010-08-28 wenzelm 2010-08-28 include Document.History in Document.State -- just one universal session state maintained by main actor; Session.command_change_buffer: thread actor ensures asynchronous dispatch; misc tuning;
2010-08-20 wenzelm 2010-08-20 tuned signatures;
2010-08-15 wenzelm 2010-08-15 some derived operations on Text.Range;
2010-08-15 wenzelm 2010-08-15 specific types Text.Offset and Text.Range; minor tuning;
2010-08-15 wenzelm 2010-08-15 moved Text_Edit to Text.Edit; tuned;
2010-08-15 wenzelm 2010-08-15 moved History/Snapshot to document.scala;
2010-08-15 wenzelm 2010-08-15 more explicit / functional ML version of document model; tuned;
2010-08-15 wenzelm 2010-08-15 renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;
2010-08-14 wenzelm 2010-08-14 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
2010-08-14 wenzelm 2010-08-14 moved Document.text_edits to Thy_Syntax;
2010-08-14 wenzelm 2010-08-14 tuned;
2010-08-13 wenzelm 2010-08-13 explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;
2010-08-12 wenzelm 2010-08-12 more basic notion of unparsed input;
2010-08-12 wenzelm 2010-08-12 simplified/clarified Change: transition prev --edits--> result, based on futures; Session.history: plain List instead of somewhat indirect Change.ancestors; tuned;
2010-08-12 wenzelm 2010-08-12 moved snapshot to Session (cf. 96b22dfeb56a);
2010-08-12 wenzelm 2010-08-12 Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway; Document.edit_text: create new document id here;
2010-08-12 wenzelm 2010-08-12 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type (ML) / Document.ID;
2010-08-12 wenzelm 2010-08-12 specific command state;
2010-08-11 wenzelm 2010-08-11 consider command state as part of Snapshot, not Document;
2010-08-11 wenzelm 2010-08-11 represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
2010-08-07 wenzelm 2010-08-07 concentrate structural document notions in document.scala; tuned;
2010-08-06 wenzelm 2010-08-06 avoid null in Scala; tuned comments;
2010-08-05 wenzelm 2010-08-05 explicit Change.Snapshot and Document.Node; misc tuning and clarification; Document_View: explicitly highlight outdated command status;
2010-08-05 wenzelm 2010-08-05 simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;
2010-07-19 wenzelm 2010-07-19 Session: predefined real time parameters; Document_View: delayed caret handling, for improved reactivity; selected_command: proper_command_at ignores ignored commands;
2010-07-03 wenzelm 2010-07-03 more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations; misc tuning;
2010-05-29 wenzelm 2010-05-29 explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;