src/Pure/PIDE/document.scala
Sat, 12 Nov 2011 19:44:56 +0100 wenzelm index markup elements for more efficient cumulate/select operations;
Sat, 12 Nov 2011 12:21:42 +0100 wenzelm tuned signature;
Sat, 12 Nov 2011 11:45:49 +0100 wenzelm tuned signature;
Fri, 11 Nov 2011 21:45:52 +0100 wenzelm added markup_cumulate operator;
Sat, 22 Oct 2011 19:00:03 +0200 wenzelm class Counter as abstract datatype;
Sun, 18 Sep 2011 00:05:22 +0200 wenzelm graph traversal in topological order;
Sat, 17 Sep 2011 23:04:03 +0200 wenzelm Document.Node.Name convenience;
Sat, 17 Sep 2011 21:28:52 +0200 wenzelm more elaborate Node_Renderer, which paints node_name.theory only;
Sat, 03 Sep 2011 21:15:35 +0200 wenzelm Document.removed_versions on Scala side;
Sat, 03 Sep 2011 12:31:27 +0200 wenzelm some support to prune_history;
Thu, 01 Sep 2011 22:29:57 +0200 wenzelm more redable Document.Node.toString;
Thu, 01 Sep 2011 13:39:40 +0200 wenzelm tuned signature;
Thu, 01 Sep 2011 13:34:45 +0200 wenzelm more abstract Document.Node.Name;
Wed, 31 Aug 2011 22:10:07 +0200 wenzelm crude display of node status;
Wed, 31 Aug 2011 15:41:22 +0200 wenzelm maintain name of *the* enclosing node as part of command -- avoid full document traversal;
Tue, 30 Aug 2011 16:04:26 +0200 wenzelm tuned signature;
Tue, 30 Aug 2011 15:49:27 +0200 wenzelm dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);
Tue, 30 Aug 2011 15:43:27 +0200 wenzelm some support for hyperlinks between different buffers;
Sat, 27 Aug 2011 12:22:24 +0200 wenzelm de-assigned commands also count as changed;
Fri, 26 Aug 2011 22:14:12 +0200 wenzelm tuned Session.edit_node: update_perspective based on last_exec_offset;
Fri, 26 Aug 2011 15:09:54 +0200 wenzelm refined document state assignment: observe perspective, more explicit assignment message;
Thu, 25 Aug 2011 17:38:12 +0200 wenzelm maintain last_execs assignment on Scala side;
Thu, 25 Aug 2011 16:44:06 +0200 wenzelm propagate information about last command with exec state assignment through document model;
Thu, 25 Aug 2011 13:24:41 +0200 wenzelm tuned signature;
Thu, 25 Aug 2011 11:41:48 +0200 wenzelm slightly more abstract Command.Perspective;
Wed, 24 Aug 2011 17:25:45 +0200 wenzelm misc tuning and simplification;
Wed, 24 Aug 2011 16:49:48 +0200 wenzelm clarified Document.Node.clear -- retain header (cf. ML version);
Wed, 24 Aug 2011 16:27:27 +0200 wenzelm clarified norm_header/header_edit -- disallow update of loaded theories;
Wed, 24 Aug 2011 13:03:39 +0200 wenzelm update_perspective without actual edits, bypassing the full state assignment protocol;
Tue, 23 Aug 2011 12:20:12 +0200 wenzelm propagate editor perspective through document model;
Mon, 22 Aug 2011 21:42:02 +0200 wenzelm some support for editor perspective;
Mon, 22 Aug 2011 21:09:26 +0200 wenzelm discontinued redundant Edit_Command_ID;
Tue, 16 Aug 2011 21:13:52 +0200 wenzelm use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
Sat, 13 Aug 2011 20:20:36 +0200 wenzelm provide node header via Scala layer;
Sat, 13 Aug 2011 16:04:28 +0200 wenzelm tuned signature;
Sat, 13 Aug 2011 15:59:26 +0200 wenzelm clarified node header -- exclude master_dir;
Fri, 12 Aug 2011 22:10:49 +0200 wenzelm normalized theory dependencies wrt. file_store;
Fri, 12 Aug 2011 15:28:30 +0200 wenzelm clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
Fri, 12 Aug 2011 12:03:17 +0200 wenzelm simplified class Thy_Header;
Thu, 11 Aug 2011 20:32:44 +0200 wenzelm uniform treatment of header edits as document edits;
Thu, 11 Aug 2011 18:01:28 +0200 wenzelm explicit datatypes for document node edits;
Tue, 12 Jul 2011 19:36:46 +0200 wenzelm more uniform Properties in ML and Scala;
Sun, 10 Jul 2011 00:21:19 +0200 wenzelm propagate header changes to prover process;
Sat, 09 Jul 2011 13:29:33 +0200 wenzelm some support for blobs (arbitrary text files) within document nodes;
Thu, 07 Jul 2011 22:04:30 +0200 wenzelm explicit Document.Node.Header, with master_dir and thy_name;
Mon, 04 Jul 2011 22:25:33 +0200 wenzelm Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
Sat, 18 Jun 2011 00:03:58 +0200 wenzelm select_markup: no filtering here -- results may be distorted anyway;
Fri, 17 Jun 2011 23:18:22 +0200 wenzelm more explicit error message;
Thu, 11 Nov 2010 17:07:05 +0100 wenzelm unified type Document.Edit;
Thu, 11 Nov 2010 16:48:46 +0100 wenzelm replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
Sat, 25 Sep 2010 13:57:34 +0200 wenzelm tuned signature;
Wed, 22 Sep 2010 22:25:21 +0200 wenzelm Snapshot.convert/revert: explicit error report to isolate sporadic crash;
Tue, 07 Sep 2010 23:06:52 +0200 wenzelm concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
Tue, 07 Sep 2010 22:28:58 +0200 wenzelm simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
Wed, 01 Sep 2010 18:18:47 +0200 wenzelm Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;
Tue, 31 Aug 2010 19:55:43 +0200 wenzelm Node.full_index: allow command spans larger than block_size;
Tue, 31 Aug 2010 17:35:41 +0200 wenzelm Document state assignment indicates command change;
Tue, 31 Aug 2010 13:20:12 +0200 wenzelm simplified/clarified Document_View.text_area_extension;
Tue, 31 Aug 2010 12:49:40 +0200 wenzelm Document.Node: significant speedup of command_range etc. via lazy full_index;
Mon, 30 Aug 2010 13:01:32 +0200 wenzelm Command.results: ordered by serial number;
less more (0) -60 tip