src/Pure/PIDE/document.scala
2011-11-12 ago tuned signature;
2011-11-12 ago tuned signature;
2011-11-11 ago added markup_cumulate operator;
2011-10-22 ago class Counter as abstract datatype;
2011-09-18 ago graph traversal in topological order;
2011-09-17 ago Document.Node.Name convenience;
2011-09-17 ago more elaborate Node_Renderer, which paints node_name.theory only;
2011-09-03 ago Document.removed_versions on Scala side;
2011-09-03 ago some support to prune_history;
2011-09-01 ago more redable Document.Node.toString;
2011-09-01 ago tuned signature;
2011-09-01 ago more abstract Document.Node.Name;
2011-08-31 ago crude display of node status;
2011-08-31 ago maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-30 ago tuned signature;
2011-08-30 ago dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);
2011-08-30 ago some support for hyperlinks between different buffers;
2011-08-27 ago de-assigned commands also count as changed;
2011-08-26 ago tuned Session.edit_node: update_perspective based on last_exec_offset;
2011-08-26 ago refined document state assignment: observe perspective, more explicit assignment message;
2011-08-25 ago maintain last_execs assignment on Scala side;
2011-08-25 ago propagate information about last command with exec state assignment through document model;
2011-08-25 ago tuned signature;
2011-08-25 ago slightly more abstract Command.Perspective;
2011-08-24 ago misc tuning and simplification;
2011-08-24 ago clarified Document.Node.clear -- retain header (cf. ML version);
2011-08-24 ago clarified norm_header/header_edit -- disallow update of loaded theories;
2011-08-24 ago update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-23 ago propagate editor perspective through document model;
2011-08-22 ago some support for editor perspective;
2011-08-22 ago discontinued redundant Edit_Command_ID;
2011-08-16 ago use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
2011-08-13 ago provide node header via Scala layer;
2011-08-13 ago tuned signature;
2011-08-13 ago clarified node header -- exclude master_dir;
2011-08-12 ago normalized theory dependencies wrt. file_store;
2011-08-12 ago clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-12 ago simplified class Thy_Header;
2011-08-11 ago uniform treatment of header edits as document edits;
2011-08-11 ago explicit datatypes for document node edits;
2011-07-12 ago more uniform Properties in ML and Scala;
2011-07-10 ago propagate header changes to prover process;
2011-07-09 ago some support for blobs (arbitrary text files) within document nodes;
2011-07-07 ago explicit Document.Node.Header, with master_dir and thy_name;
2011-07-04 ago Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-06-18 ago select_markup: no filtering here -- results may be distorted anyway;
2011-06-17 ago more explicit error message;
2010-11-11 ago unified type Document.Edit;
2010-11-11 ago replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
2010-09-25 ago tuned signature;
2010-09-22 ago Snapshot.convert/revert: explicit error report to isolate sporadic crash;
2010-09-07 ago concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
2010-09-07 ago simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
2010-09-01 ago Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;
2010-08-31 ago Node.full_index: allow command spans larger than block_size;
2010-08-31 ago Document state assignment indicates command change;
2010-08-31 ago simplified/clarified Document_View.text_area_extension;
2010-08-31 ago Document.Node: significant speedup of command_range etc. via lazy full_index;
2010-08-30 ago Command.results: ordered by serial number;
2010-08-29 ago use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;