tuned signature;

tuned;

less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);

clarified signature;

tuned signature;

normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;

proper edits;

tuned signature;

discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;

proper treatment of line that becomes empty;

clarified Document.offset: including final position;
support Document.change according to VSCode;

support for semantic completion;

more explocit Document_Model.Content;

tuned;

clarified lazy text content;

Line.Document consists of independently allocated strings;
tuned signature;

more robust treatment of logical lines;

manage document blobs as well;

proper line_offset;

clarified Document.length -- independent of text_length;

unused;

precise full_range and thus proper try_restrict in Snapshot.cumulate;

clarified signature: maintan Text.Length within Line.Document;

clarified modules;

clarified signature: explicit Length to avoid implicit mistakes;

more uniform treatment of input/output wrt. client;
support for diagnistic messages;
misc tuning;

clarified document: no stored text;

tuned;

clarified signature;

tuned signature;

tuned signature -- more explicit types;

clarified border cases;

proper reset of column (amending 01e50039edc9);

more systematic text length wrt. encoding;

more systematic text length;

unused;

clarified modules;

--HG--
rename : src/Tools/VSCode/src/line.scala => src/Pure/PIDE/line.scala