src/Pure/PIDE/text.scala
2010-08-26 wenzelm 2010-08-26 tuned signature;
2010-08-24 wenzelm 2010-08-24 Text.Range.is_singleton;
2010-08-22 wenzelm 2010-08-22 misc tuning and simplification;
2010-08-22 wenzelm 2010-08-22 renamed Markup_Tree.Node to Text.Info; Markup_Tree.select: body may depend on full Text.Info, including range; tuned;
2010-08-20 wenzelm 2010-08-20 added Text.Range.- convenience;
2010-08-20 wenzelm 2010-08-20 alternative constructor for Range singularities;
2010-08-20 wenzelm 2010-08-20 further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
2010-08-19 wenzelm 2010-08-19 parameterized type Markup_Tree.Node; Markup_Tree.select: allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;
2010-08-19 wenzelm 2010-08-19 added toString methods;
2010-08-19 wenzelm 2010-08-19 misc tuning and simplification;
2010-08-19 wenzelm 2010-08-19 Text.Range: improved handling of singularities;
2010-08-18 wenzelm 2010-08-18 refined notion of Text.Range;
2010-08-15 wenzelm 2010-08-15 some derived operations on Text.Range;
2010-08-15 wenzelm 2010-08-15 specific types Text.Offset and Text.Range; minor tuning;
2010-08-15 wenzelm 2010-08-15 moved Text_Edit to Text.Edit; tuned;