src/Pure/PIDE/command.scala
2010-08-15 wenzelm 2010-08-15 specific types Text.Offset and Text.Range; minor tuning;
2010-08-14 wenzelm 2010-08-14 Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
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 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;
2010-08-12 wenzelm 2010-08-12 misc tuning and simplification;
2010-08-12 wenzelm 2010-08-12 specific command state;
2010-08-12 wenzelm 2010-08-12 specific Session.Commands_Changed;
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-06 wenzelm 2010-08-06 avoid null in Scala; tuned comments;
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-06-13 wenzelm 2010-06-13 tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
2010-05-30 wenzelm 2010-05-30 more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;
2010-05-29 wenzelm 2010-05-29 tuned messages;
2010-05-28 wenzelm 2010-05-28 accumulate only local results -- no proper history support yet;
2010-05-27 wenzelm 2010-05-27 Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);
2010-05-20 wenzelm 2010-05-20 explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-05 wenzelm 2010-05-05 some rearrangement of Scala sources;