src/Pure/PIDE/document.ML
Sat, 06 Nov 2010 20:59:59 +0100 wenzelm continue after failed commands;
Sat, 06 Nov 2010 16:31:35 +0100 wenzelm explicit "timing" status for toplevel transactions;
Sat, 06 Nov 2010 16:03:49 +0100 wenzelm tuned;
Wed, 15 Sep 2010 16:06:52 +0200 wenzelm Document.async_state: some attempts to make this more robust wrt. cancelation of the main transaction -- avoid confusing feedback about pending forks;
Thu, 09 Sep 2010 18:21:06 +0200 wenzelm refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Tue, 31 Aug 2010 23:46:49 +0200 wenzelm moved Toplevel.run_command to Pure/PIDE/document.ML;
Mon, 30 Aug 2010 14:56:27 +0200 wenzelm tuned;
Tue, 17 Aug 2010 15:54:04 +0200 wenzelm tune;
Tue, 17 Aug 2010 15:10:49 +0200 wenzelm added functor Linear_Set, based on former adhoc structures in document.ML;
Sun, 15 Aug 2010 20:13:07 +0200 wenzelm document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
Sun, 15 Aug 2010 19:30:11 +0200 wenzelm renamed create_id to new_id;
Sun, 15 Aug 2010 18:41:23 +0200 wenzelm more explicit / functional ML version of document model;
Sat, 14 Aug 2010 22:45:23 +0200 wenzelm more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
Sat, 14 Aug 2010 11:52:24 +0200 wenzelm tuned;
Thu, 12 Aug 2010 15:19:11 +0200 wenzelm clarified "state" (accumulated data) vs. "exec" (execution that produces data);
Wed, 11 Aug 2010 22:41:26 +0200 wenzelm represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
Thu, 05 Aug 2010 14:35:35 +0200 wenzelm simplified/refined document model: collection of named nodes, without proper dependencies yet;
less more (0) tip