src/Pure/PIDE/text.scala
14 months ago wenzelm 2016-12-10 clarified output: avoid confusion with line:column notation;
16 months ago wenzelm 2016-10-24 discontinued unused / untested distinction of separate PIDE modules;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2014-10-21 wenzelm 2014-10-21 some structure matching, based on line token iterators;
2014-08-12 wenzelm 2014-08-12 tuned;
2014-07-23 wenzelm 2014-07-23 more explicit treatment of cleared nodes (removal is implicit);
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-15 wenzelm 2014-04-15 clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
2014-04-08 wenzelm 2014-04-08 simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway;
2014-04-08 wenzelm 2014-04-08 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
2014-04-08 wenzelm 2014-04-08 avoid data redundancy;
2014-04-08 wenzelm 2014-04-08 tuned signature -- moved Command.Chunk to Text.Chunk;
2014-03-27 wenzelm 2014-03-27 tuned;
2014-03-17 wenzelm 2014-03-17 tuned signature;
2012-08-04 wenzelm 2012-08-04 tuned import;
2012-04-18 wenzelm 2012-04-18 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 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-02-21 wenzelm 2012-02-21 approximate Perspective.full within the bounds of the JVM;
2012-01-14 wenzelm 2012-01-14 clarified partial restrict operation;
2011-11-29 wenzelm 2011-11-29 separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 wenzelm 2011-11-28 explicit indication of modules for independent Scala library;
2011-11-25 wenzelm 2011-11-25 recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
2011-11-12 wenzelm 2011-11-12 more precise type;
2011-11-11 wenzelm 2011-11-11 prefer statically typed Text.Markup;
2011-10-22 wenzelm 2011-10-22 class Text.Edit as abstract datatype;
2011-10-21 wenzelm 2011-10-21 proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views); clarified Text.Range apartness, with try_restrict and try_join operations; private Perspective constructor to ensure abstract datatype integrity;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Command.Perspective;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Text.Perspective;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-08-22 wenzelm 2011-08-22 added official Text.Range.Ordering; some support for text perspective;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-07-04 wenzelm 2011-07-04 imitate exception ERROR of Isabelle/ML;
2011-06-18 wenzelm 2011-06-18 more robust treatment of partial range restriction;
2011-06-17 wenzelm 2011-06-17 more explicit error message; convert/revert range; tuned;
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;