src/Pure/PIDE/document.scala
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 Markup_Tree.select: 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.; Markup_Tree.select: 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 Document.id (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;
2010-05-24 wenzelm 2010-05-24 @tailrec annotation;
2010-05-24 wenzelm 2010-05-24 renamed "rev" to "reverse" following usual Scala conventions;
2010-05-22 wenzelm 2010-05-22 parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
2010-05-22 wenzelm 2010-05-22 removed timing;
2010-05-20 wenzelm 2010-05-20 explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-17 wenzelm 2010-05-17 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
2010-05-08 wenzelm 2010-05-08 removed junk;
2010-05-05 wenzelm 2010-05-05 some rearrangement of Scala sources;