src/Pure/Isar/isar_document.ML
Tue, 20 Jul 2010 20:10:27 +0200 wenzelm execute document version at high priority;
Tue, 20 Jul 2010 18:19:50 +0200 wenzelm edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sat, 29 May 2010 16:44:44 +0200 wenzelm define_state/new_state: provide state immediately, which is now lazy;
Thu, 27 May 2010 21:14:53 +0200 wenzelm substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
Thu, 27 May 2010 20:15:36 +0200 wenzelm further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
Sat, 15 May 2010 23:40:00 +0200 wenzelm renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
Sat, 15 May 2010 23:23:45 +0200 wenzelm renamed structure ValueParse to Parse_Value;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Wed, 06 Jan 2010 23:18:12 +0100 wenzelm always report updates -- required has "handshake";
Mon, 04 Jan 2010 18:56:36 +0100 wenzelm explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
Wed, 30 Dec 2009 21:32:25 +0100 wenzelm eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
Tue, 29 Dec 2009 20:59:47 +0100 wenzelm back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
Tue, 29 Dec 2009 20:30:40 +0100 wenzelm removed slightly odd Isar_Document.init;
Tue, 27 Oct 2009 13:16:16 +0100 wenzelm non-critical atomic accesses;
Wed, 30 Sep 2009 23:16:15 +0200 wenzelm actually perform Isar_Document.init on startup;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 15 Sep 2009 15:17:53 +0200 wenzelm Isar.define_command: identify transaction;
Tue, 01 Sep 2009 14:51:40 +0200 wenzelm modernized Isar_Document;
Thu, 04 Jun 2009 22:52:53 +0200 wenzelm uniform (short) ids on both sides;
Fri, 16 Jan 2009 21:24:33 +0100 wenzelm define_state: use empty_state;
Fri, 16 Jan 2009 16:00:20 +0100 wenzelm provide end_document;
Fri, 16 Jan 2009 15:21:26 +0100 wenzelm run command: check theory name for init;
Fri, 16 Jan 2009 12:10:51 +0100 wenzelm fold_entries: non-optional start, permissive;
Thu, 15 Jan 2009 15:51:19 +0100 wenzelm command 'Isar.edit_document': actually invoke edit_document;
Thu, 15 Jan 2009 12:16:51 +0100 wenzelm tuned;
Thu, 15 Jan 2009 11:55:22 +0100 wenzelm edit_document: proper edits/edit markup, including the document id;
Thu, 15 Jan 2009 00:48:45 +0100 wenzelm removed junk;
Thu, 15 Jan 2009 00:44:06 +0100 wenzelm misc cleanup and simplification;
Tue, 13 Jan 2009 22:20:49 +0100 wenzelm misc internal rearrangements;
Tue, 13 Jan 2009 17:34:12 +0100 wenzelm replaced sys_error by plain error;
Tue, 13 Jan 2009 13:47:35 +0100 wenzelm added Isar/isar_document.ML: Interactive Isar documents.
less more (0) tip