src/Pure/PIDE/document.ML
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