src/Pure/PIDE/text.scala
2017-06-19 ago clarified signature;
2017-04-20 ago tuned signature;
2017-04-04 ago tuned signature;
2017-03-12 ago discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
2017-03-08 ago suppress vacuous edits;
2017-03-08 ago clarified native Text.Offset versus Text.Length index Int;
2017-03-08 ago tuned;
2017-03-06 ago tuned;
2017-01-07 ago tuned;
2016-12-28 ago clarified modules;
2016-12-28 ago tuned;
2016-12-10 ago clarified output: avoid confusion with line:column notation;
2016-10-24 ago discontinued unused / untested distinction of separate PIDE modules;
2015-05-03 ago misc tuning, based on warnings by IntelliJ IDEA;
2014-10-21 ago some structure matching, based on line token iterators;
2014-08-12 ago tuned;
2014-07-23 ago more explicit treatment of cleared nodes (removal is implicit);
2014-04-26 ago tuned signature;
2014-04-15 ago clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
2014-04-08 ago simplified Text.Chunk -- eliminated ooddities;
2014-04-08 ago accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
2014-04-08 ago avoid data redundancy;
2014-04-08 ago tuned signature -- moved Command.Chunk to Text.Chunk;
2014-03-27 ago tuned;
2014-03-17 ago tuned signature;
2012-08-04 ago tuned import;
2012-04-18 ago more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
2012-02-27 ago prefer final ADTs -- prevent ooddities;
2012-02-21 ago approximate Perspective.full within the bounds of the JVM;
2012-01-14 ago clarified partial restrict operation;
2011-11-29 ago separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 ago explicit indication of modules for independent Scala library;
2011-11-25 ago recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
2011-11-12 ago more precise type;
2011-11-11 ago prefer statically typed Text.Markup;
2011-10-22 ago class Text.Edit as abstract datatype;
2011-10-21 ago proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
2011-08-25 ago slightly more abstract Command.Perspective;
2011-08-25 ago slightly more abstract Text.Perspective;
2011-08-22 ago some support for editor perspective;
2011-08-22 ago added official Text.Range.Ordering;
2011-07-09 ago tuned signature;
2011-07-04 ago imitate exception ERROR of Isabelle/ML;
2011-06-18 ago more robust treatment of partial range restriction;
2011-06-17 ago more explicit error message;
2010-08-26 ago tuned signature;
2010-08-24 ago Text.Range.is_singleton;
2010-08-22 ago misc tuning and simplification;
2010-08-22 ago renamed Markup_Tree.Node to Text.Info;
2010-08-20 ago added Text.Range.- convenience;
2010-08-20 ago alternative constructor for Range singularities;
2010-08-20 ago further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
2010-08-19 ago parameterized type Markup_Tree.Node;
2010-08-19 ago added toString methods;
2010-08-19 ago misc tuning and simplification;
2010-08-19 ago Text.Range: improved handling of singularities;
2010-08-18 ago refined notion of Text.Range;
2010-08-15 ago some derived operations on Text.Range;
2010-08-15 ago specific types Text.Offset and Text.Range;
2010-08-15 ago moved Text_Edit to Text.Edit;