| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2010 23:18:12 +0100 |
wenzelm |
always report updates -- required has "handshake";
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 18:56:36 +0100 |
wenzelm |
explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2009 20:59:47 +0100 |
wenzelm |
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2009 20:30:40 +0100 |
wenzelm |
removed slightly odd Isar_Document.init;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 13:16:16 +0100 |
wenzelm |
non-critical atomic accesses;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 23:16:15 +0200 |
wenzelm |
actually perform Isar_Document.init on startup;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 15:17:53 +0200 |
wenzelm |
Isar.define_command: identify transaction;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 14:51:40 +0200 |
wenzelm |
modernized Isar_Document;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 22:52:53 +0200 |
wenzelm |
uniform (short) ids on both sides;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 21:24:33 +0100 |
wenzelm |
define_state: use empty_state;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 16:00:20 +0100 |
wenzelm |
provide end_document;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 15:21:26 +0100 |
wenzelm |
run command: check theory name for init;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 12:10:51 +0100 |
wenzelm |
fold_entries: non-optional start, permissive;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 15:51:19 +0100 |
wenzelm |
command 'Isar.edit_document': actually invoke edit_document;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 12:16:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 11:55:22 +0100 |
wenzelm |
edit_document: proper edits/edit markup, including the document id;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 00:48:45 +0100 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 00:44:06 +0100 |
wenzelm |
misc cleanup and simplification;
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 22:20:49 +0100 |
wenzelm |
misc internal rearrangements;
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 17:34:12 +0100 |
wenzelm |
replaced sys_error by plain error;
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 13:47:35 +0100 |
wenzelm |
added Isar/isar_document.ML: Interactive Isar documents.
|
file |
diff |
annotate
|