src/Pure/PIDE/line.scala
20 months ago ago tuned signature;
21 months ago ago tuned;
22 months ago ago less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
2017-05-22 ago clarified signature;
2017-04-20 ago tuned signature;
2017-03-14 ago normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
2017-03-12 ago proper edits;
2017-03-12 ago tuned signature;
2017-03-12 ago discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
2017-03-09 ago proper treatment of line that becomes empty;
2017-03-09 ago clarified Document.offset: including final position;
2017-01-11 ago support for semantic completion;
2017-01-08 ago more explocit Document_Model.Content;
2017-01-07 ago tuned;
2017-01-07 ago clarified lazy text content;
2017-01-07 ago Line.Document consists of independently allocated strings;
2017-01-05 ago more robust treatment of logical lines;
2017-01-05 ago manage document blobs as well;
2017-01-03 ago proper line_offset;
2016-12-29 ago clarified Document.length -- independent of text_length;
2016-12-28 ago unused;
2016-12-28 ago precise full_range and thus proper try_restrict in Snapshot.cumulate;
2016-12-28 ago clarified signature: maintan Text.Length within Line.Document;
2016-12-28 ago clarified modules;
2016-12-28 ago clarified signature: explicit Length to avoid implicit mistakes;
2016-12-28 ago more uniform treatment of input/output wrt. client;
2016-12-26 ago clarified document: no stored text;
2016-12-23 ago tuned;
2016-12-21 ago clarified signature;
2016-12-21 ago tuned signature;
2016-12-21 ago tuned signature -- more explicit types;
2016-12-21 ago clarified border cases;
2016-12-20 ago proper reset of column (amending 01e50039edc9);
2016-12-20 ago more systematic text length wrt. encoding;
2016-12-20 ago more systematic text length;
2016-12-20 ago unused;
2016-12-20 ago clarified modules;