src/Pure/PIDE/isar_document.scala
Fri, 02 Sep 2011 11:52:13 +0200 wenzelm clarified define_command: store name as structural information;
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 20:47:33 +0200 wenzelm explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
Fri, 26 Aug 2011 16:06:58 +0200 wenzelm tuned signature;
Fri, 26 Aug 2011 15:09:54 +0200 wenzelm refined document state assignment: observe perspective, more explicit assignment message;
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 11:41:48 +0200 wenzelm slightly more abstract Command.Perspective;
Wed, 24 Aug 2011 13:03:39 +0200 wenzelm update_perspective without actual edits, bypassing the full state assignment protocol;
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;
Sat, 13 Aug 2011 20:20:36 +0200 wenzelm provide node header via Scala layer;
Sat, 13 Aug 2011 15:59:26 +0200 wenzelm clarified node header -- exclude master_dir;
Fri, 12 Aug 2011 12:03:17 +0200 wenzelm simplified class Thy_Header;
Fri, 12 Aug 2011 11:41:26 +0200 wenzelm clarified Exn.message;
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 10:44:30 +0200 wenzelm tuned XML modules;
Mon, 11 Jul 2011 16:48:02 +0200 wenzelm JVM method invocation service via Scala layer;
Sun, 10 Jul 2011 20:59:04 +0200 wenzelm inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
Sun, 10 Jul 2011 13:51:21 +0200 wenzelm simplified XML_Data;
Sun, 10 Jul 2011 13:00:22 +0200 wenzelm less currying in Scala;
Sun, 10 Jul 2011 00:21:19 +0200 wenzelm propagate header changes to prover process;
Thu, 11 Nov 2010 17:07:05 +0100 wenzelm unified type Document.Edit;
Thu, 23 Sep 2010 15:36:03 +0200 wenzelm tuned;
Thu, 23 Sep 2010 14:39:29 +0200 wenzelm tuned prover message categorization;
Wed, 22 Sep 2010 22:39:17 +0200 wenzelm Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
Fri, 17 Sep 2010 21:49:34 +0200 wenzelm some specific message classification;
Fri, 17 Sep 2010 17:10:44 +0200 wenzelm allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
Fri, 17 Sep 2010 15:51:11 +0200 wenzelm eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
Tue, 07 Sep 2010 23:59:14 +0200 wenzelm Document_View: select gutter message icons from markup over line range, not full range results;
Tue, 07 Sep 2010 18:44:28 +0200 wenzelm basic support for warning/error gutter icons;
Tue, 07 Sep 2010 16:40:30 +0200 wenzelm Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
Tue, 07 Sep 2010 15:03:59 +0200 wenzelm Isar_Document.reported_positions: exclude proof state output;
Thu, 02 Sep 2010 23:26:21 +0200 wenzelm Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
Tue, 31 Aug 2010 23:28:21 +0200 wenzelm Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
Sun, 22 Aug 2010 20:11:17 +0200 wenzelm simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
Fri, 20 Aug 2010 11:57:43 +0200 wenzelm concentrate protocol message formats in Isar_Document;
Thu, 19 Aug 2010 12:51:48 +0200 wenzelm moved Isar_Document to Pure/PIDE;
less more (0) tip