src/Pure/PIDE/document.scala
Tue, 08 Apr 2014 15:12:54 +0200 wenzelm tuned signature -- moved Command.Chunk to Text.Chunk;
Tue, 08 Apr 2014 12:19:33 +0200 wenzelm more explicit Command.Chunk types, less ooddities;
Fri, 04 Apr 2014 10:41:53 +0200 wenzelm afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
Thu, 03 Apr 2014 21:08:00 +0200 wenzelm clarified Version.syntax -- avoid guessing initial situation;
Thu, 03 Apr 2014 20:53:35 +0200 wenzelm more abstract Prover.Syntax, as proposed by Carst Tankink;
Wed, 02 Apr 2014 20:41:44 +0200 wenzelm tuned signature -- more explicit iterator terminology;
Wed, 02 Apr 2014 20:22:12 +0200 wenzelm more explicit iterator terminology, in accordance to Scala 2.8 library;
Tue, 01 Apr 2014 20:22:25 +0200 wenzelm more direct command states -- merge_results is hardly ever needed;
Mon, 31 Mar 2014 15:34:37 +0200 wenzelm tuned output;
Mon, 31 Mar 2014 15:28:14 +0200 wenzelm tuned signature -- more static typing;
Mon, 31 Mar 2014 15:05:24 +0200 wenzelm store blob content within document node: aux. files that were once open are made persistent;
Sat, 29 Mar 2014 09:34:51 +0100 wenzelm tuned signature;
Thu, 27 Mar 2014 21:18:14 +0100 wenzelm tuned -- avoid code duplication;
Thu, 27 Mar 2014 12:11:32 +0100 wenzelm more frugal merge of markup trees: filter wrt. subsequent query;
Thu, 27 Mar 2014 11:19:31 +0100 wenzelm tuned signature;
Thu, 27 Mar 2014 10:43:43 +0100 wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
Wed, 26 Mar 2014 21:01:09 +0100 wenzelm tuned signature -- expose less intermediate information;
Wed, 26 Mar 2014 19:42:16 +0100 wenzelm clarified valid_id: always standardize towards static command.id;
Mon, 17 Mar 2014 14:37:23 +0100 wenzelm tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
Sat, 01 Mar 2014 12:07:26 +0100 wenzelm tuned signature -- more explicit Document.Elements;
Fri, 28 Feb 2014 11:58:26 +0100 wenzelm tuned data structure;
Fri, 28 Feb 2014 11:50:54 +0100 wenzelm tuned;
Thu, 27 Feb 2014 14:07:04 +0100 wenzelm more formal Document.Blobs;
Thu, 27 Feb 2014 12:48:59 +0100 wenzelm tuned output;
Wed, 26 Feb 2014 20:56:55 +0100 wenzelm tuned output;
Mon, 24 Feb 2014 11:05:02 +0100 wenzelm tuned messages;
Fri, 21 Feb 2014 15:48:04 +0100 wenzelm tuned signature -- avoid redundancy and confusion of flags;
Fri, 21 Feb 2014 15:22:06 +0100 wenzelm tuned signature;
Fri, 21 Feb 2014 15:12:50 +0100 wenzelm more general / abstract Command.Markups, with separate index for status elements;
Thu, 20 Feb 2014 16:00:37 +0100 wenzelm cumulate/select wrt. precise elements guard;
less more (0) -100 -50 -30 tip