#
5d104916 |
|
06-Oct-2019 |
wenzelm <none@none> |
tuned signature;
|
#
7a11ac1e |
|
06-Nov-2017 |
wenzelm <none@none> |
tuned signature;
|
#
6da03ca3 |
|
27-Oct-2017 |
wenzelm <none@none> |
tuned;
|
#
cbcb9b75 |
|
05-Sep-2017 |
wenzelm <none@none> |
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
|
#
057fcdaf |
|
22-May-2017 |
wenzelm <none@none> |
clarified signature;
|
#
1a2ae8bf |
|
20-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
dc55f62e |
|
14-Mar-2017 |
wenzelm <none@none> |
normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
|
#
d5489db6 |
|
12-Mar-2017 |
wenzelm <none@none> |
proper edits;
|
#
2cbeb484 |
|
12-Mar-2017 |
wenzelm <none@none> |
tuned signature;
|
#
65cade08 |
|
12-Mar-2017 |
wenzelm <none@none> |
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
|
#
6687dcb6 |
|
09-Mar-2017 |
wenzelm <none@none> |
proper treatment of line that becomes empty;
|
#
7de8006c |
|
09-Mar-2017 |
wenzelm <none@none> |
clarified Document.offset: including final position; support Document.change according to VSCode;
|
#
19cde84c |
|
11-Jan-2017 |
wenzelm <none@none> |
support for semantic completion;
|
#
78b65853 |
|
07-Jan-2017 |
wenzelm <none@none> |
more explocit Document_Model.Content;
|
#
c83c03cf |
|
07-Jan-2017 |
wenzelm <none@none> |
tuned;
|
#
dd04f103 |
|
07-Jan-2017 |
wenzelm <none@none> |
clarified lazy text content;
|
#
a1afe236 |
|
07-Jan-2017 |
wenzelm <none@none> |
Line.Document consists of independently allocated strings; tuned signature;
|
#
fdadc7da |
|
05-Jan-2017 |
wenzelm <none@none> |
more robust treatment of logical lines;
|
#
18a411fb |
|
05-Jan-2017 |
wenzelm <none@none> |
manage document blobs as well;
|
#
c4ea2661 |
|
03-Jan-2017 |
wenzelm <none@none> |
proper line_offset;
|
#
d93a9620 |
|
29-Dec-2016 |
wenzelm <none@none> |
clarified Document.length -- independent of text_length;
|
#
5082f2c4 |
|
28-Dec-2016 |
wenzelm <none@none> |
unused;
|
#
dab7b7af |
|
28-Dec-2016 |
wenzelm <none@none> |
precise full_range and thus proper try_restrict in Snapshot.cumulate;
|
#
0fa7e0e2 |
|
28-Dec-2016 |
wenzelm <none@none> |
clarified signature: maintan Text.Length within Line.Document;
|
#
302ad5fc |
|
28-Dec-2016 |
wenzelm <none@none> |
clarified modules;
|
#
b56fd855 |
|
28-Dec-2016 |
wenzelm <none@none> |
clarified signature: explicit Length to avoid implicit mistakes;
|
#
a5f150ae |
|
28-Dec-2016 |
wenzelm <none@none> |
more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning;
|
#
458f0aa4 |
|
26-Dec-2016 |
wenzelm <none@none> |
clarified document: no stored text;
|
#
d42bbc71 |
|
23-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
1539de66 |
|
21-Dec-2016 |
wenzelm <none@none> |
clarified signature;
|
#
5b3fb67f |
|
21-Dec-2016 |
wenzelm <none@none> |
tuned signature;
|
#
3a1766d2 |
|
21-Dec-2016 |
wenzelm <none@none> |
tuned signature -- more explicit types;
|
#
fe3e7193 |
|
21-Dec-2016 |
wenzelm <none@none> |
clarified border cases;
|
#
8fd85a58 |
|
20-Dec-2016 |
wenzelm <none@none> |
proper reset of column (amending 01e50039edc9);
|
#
e38e1f2f |
|
20-Dec-2016 |
wenzelm <none@none> |
more systematic text length wrt. encoding;
|
#
44f69241 |
|
20-Dec-2016 |
wenzelm <none@none> |
more systematic text length;
|
#
bbda0449 |
|
20-Dec-2016 |
wenzelm <none@none> |
unused;
|
#
825132a4 |
|
20-Dec-2016 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Tools/VSCode/src/line.scala => src/Pure/PIDE/line.scala
|