src/Pure/PIDE/line.scala
Thu, 05 Jan 2017 21:34:04 +0100 wenzelm more robust treatment of logical lines;
Thu, 05 Jan 2017 15:15:51 +0100 wenzelm manage document blobs as well;
Tue, 03 Jan 2017 17:21:37 +0100 wenzelm proper line_offset;
Thu, 29 Dec 2016 16:00:29 +0100 wenzelm clarified Document.length -- independent of text_length;
Wed, 28 Dec 2016 19:16:45 +0100 wenzelm unused;
Wed, 28 Dec 2016 19:15:52 +0100 wenzelm precise full_range and thus proper try_restrict in Snapshot.cumulate;
Wed, 28 Dec 2016 17:26:38 +0100 wenzelm clarified signature: maintan Text.Length within Line.Document;
Wed, 28 Dec 2016 17:10:09 +0100 wenzelm clarified modules;
Wed, 28 Dec 2016 17:02:38 +0100 wenzelm clarified signature: explicit Length to avoid implicit mistakes;
Wed, 28 Dec 2016 16:45:00 +0100 wenzelm more uniform treatment of input/output wrt. client;
Mon, 26 Dec 2016 13:28:37 +0100 wenzelm clarified document: no stored text;
Fri, 23 Dec 2016 19:07:54 +0100 wenzelm tuned;
Wed, 21 Dec 2016 22:49:53 +0100 wenzelm clarified signature;
Wed, 21 Dec 2016 22:37:53 +0100 wenzelm tuned signature;
Wed, 21 Dec 2016 22:27:38 +0100 wenzelm tuned signature -- more explicit types;
Wed, 21 Dec 2016 21:17:44 +0100 wenzelm clarified border cases;
Tue, 20 Dec 2016 17:46:44 +0100 wenzelm proper reset of column (amending 01e50039edc9);
Tue, 20 Dec 2016 16:08:02 +0100 wenzelm more systematic text length wrt. encoding;
Tue, 20 Dec 2016 10:44:36 +0100 wenzelm more systematic text length;
Tue, 20 Dec 2016 10:06:18 +0100 wenzelm unused;
Tue, 20 Dec 2016 08:57:03 +0100 wenzelm clarified modules;
less more (0) tip