Mon, 16 Aug 2010 17:04:22 +0200 wenzelm simplified internal message format: dropped special Symbol.STX header;
Mon, 16 Aug 2010 16:24:22 +0200 wenzelm HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
Mon, 16 Aug 2010 12:33:52 +0200 wenzelm merged
Mon, 16 Aug 2010 12:11:01 +0200 haftmann merged
Mon, 16 Aug 2010 11:18:28 +0200 haftmann tuned section on predicate compiler
Mon, 16 Aug 2010 10:54:08 +0200 haftmann section "if something goes utterly wrong"
Mon, 16 Aug 2010 10:32:45 +0200 haftmann merged
Mon, 16 Aug 2010 10:32:35 +0200 haftmann merged
Mon, 16 Aug 2010 10:32:14 +0200 haftmann adaptation to new outline
Fri, 13 Aug 2010 17:17:16 +0200 haftmann merged
Fri, 13 Aug 2010 17:17:04 +0200 haftmann corrected handling of `constrains` elements
Mon, 16 Aug 2010 10:05:00 +0100 kleing removed non-BSD compatible option from cp
Mon, 16 Aug 2010 09:39:05 +0200 blanchet Geoff's formatter now needs closed formulas
Sun, 15 Aug 2010 17:14:10 +0200 nipkow Using type real does not require a separate logic now.
Sun, 15 Aug 2010 16:48:58 +0200 nipkow merged
Sun, 15 Aug 2010 16:48:42 +0200 nipkow tuned text about "value" and added note on comments.
Mon, 16 Aug 2010 00:07:28 +0200 wenzelm simplified command status: interpret stacked markup on demand;
Sun, 15 Aug 2010 23:13:56 +0200 wenzelm event_bus.scala rather belongs to system plumbing;
Sun, 15 Aug 2010 23:07:22 +0200 wenzelm some derived operations on Text.Range;
Sun, 15 Aug 2010 22:48:56 +0200 wenzelm specific types Text.Offset and Text.Range;
Sun, 15 Aug 2010 21:42:13 +0200 wenzelm moved Text_Edit to Text.Edit;
Sun, 15 Aug 2010 21:03:13 +0200 wenzelm moved History/Snapshot to document.scala;
Sun, 15 Aug 2010 20:27:29 +0200 wenzelm renamed raw_results to raw_protocol;
Sun, 15 Aug 2010 20:19:56 +0200 wenzelm rename "unit" to "atom", to avoid confusion with the unit type;
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:36:13 +0200 wenzelm use Synchronized.var and prevent global CRITICAL sections in this hot spot;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip