src/Pure/PIDE/isar_document.ML
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sun, 18 Sep 2011 19:49:35 +0200 wenzelm explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
Sat, 03 Sep 2011 21:15:35 +0200 wenzelm Document.removed_versions on Scala side;
Sat, 03 Sep 2011 18:08:09 +0200 wenzelm Document.remove_versions on ML side;
Fri, 02 Sep 2011 21:48:27 +0200 wenzelm raw message function "assign_execs" avoids full overhead of decoding and caching message body;
Fri, 02 Sep 2011 21:06:05 +0200 wenzelm less agressive parsing of commands (priority ~1);
Fri, 02 Sep 2011 11:52:13 +0200 wenzelm clarified define_command: store name as structural information;
Wed, 31 Aug 2011 20:47:33 +0200 wenzelm explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
Wed, 31 Aug 2011 19:52:13 +0200 wenzelm tuned join_commands: avoid traversing cumulative table;
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;
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;
Fri, 19 Aug 2011 17:39:37 +0200 wenzelm tuned signature (again);
Fri, 19 Aug 2011 15:56:26 +0200 wenzelm refined Future.cancel: explicit future allows to join actual cancellation;
Mon, 15 Aug 2011 16:38:42 +0200 wenzelm refined Document.edit: less stateful update via Graph.schedule;
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;
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 00:21:19 +0200 wenzelm propagate header changes to prover process;
Fri, 08 Jul 2011 22:00:53 +0200 wenzelm moved global state to structure Document (again);
Tue, 05 Jul 2011 20:36:49 +0200 wenzelm get theory from last executation state;
Tue, 05 Jul 2011 11:45:48 +0200 wenzelm clarified cancel_execution/await_cancellation;
Tue, 05 Jul 2011 11:16:37 +0200 wenzelm tuned signature;
Thu, 27 Jan 2011 12:24:00 +0100 wenzelm cancel document execution before editing, to improve reactivity on systems with few cores;
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