src/Pure/PIDE/document.scala
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;