src/Pure/PIDE/text.scala
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;