src/Pure/PIDE/text.scala
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Tue, 21 Oct 2014 17:49:51 +0200 wenzelm some structure matching, based on line token iterators;
Tue, 12 Aug 2014 15:46:20 +0200 wenzelm tuned;
Wed, 23 Jul 2014 16:20:07 +0200 wenzelm more explicit treatment of cleared nodes (removal is implicit);
Sat, 26 Apr 2014 13:34:10 +0200 wenzelm tuned signature;
Tue, 15 Apr 2014 16:44:06 +0200 wenzelm clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
Tue, 08 Apr 2014 20:03:00 +0200 wenzelm simplified Text.Chunk -- eliminated ooddities;
Tue, 08 Apr 2014 19:17:28 +0200 wenzelm accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
Tue, 08 Apr 2014 16:07:02 +0200 wenzelm avoid data redundancy;
Tue, 08 Apr 2014 15:12:54 +0200 wenzelm tuned signature -- moved Command.Chunk to Text.Chunk;
Thu, 27 Mar 2014 21:16:08 +0100 wenzelm tuned;
Mon, 17 Mar 2014 11:39:46 +0100 wenzelm tuned signature;
Sat, 04 Aug 2012 21:48:09 +0200 wenzelm tuned import;
Wed, 18 Apr 2012 20:22:44 +0200 wenzelm more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Tue, 21 Feb 2012 17:08:32 +0100 wenzelm approximate Perspective.full within the bounds of the JVM;
Sat, 14 Jan 2012 14:34:42 +0100 wenzelm clarified partial restrict operation;
Tue, 29 Nov 2011 21:29:53 +0100 wenzelm separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
Mon, 28 Nov 2011 22:18:19 +0100 wenzelm explicit indication of modules for independent Scala library;
Fri, 25 Nov 2011 14:23:36 +0100 wenzelm recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
Sat, 12 Nov 2011 17:52:28 +0100 wenzelm more precise type;
Fri, 11 Nov 2011 14:24:38 +0100 wenzelm prefer statically typed Text.Markup;
Sat, 22 Oct 2011 23:29:44 +0200 wenzelm class Text.Edit as abstract datatype;
Fri, 21 Oct 2011 22:44:55 +0200 wenzelm proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
Thu, 25 Aug 2011 11:41:48 +0200 wenzelm slightly more abstract Command.Perspective;
Thu, 25 Aug 2011 11:27:37 +0200 wenzelm slightly more abstract Text.Perspective;
Mon, 22 Aug 2011 21:42:02 +0200 wenzelm some support for editor perspective;
Mon, 22 Aug 2011 16:12:23 +0200 wenzelm added official Text.Range.Ordering;
Sat, 09 Jul 2011 12:56:51 +0200 wenzelm tuned signature;
Mon, 04 Jul 2011 13:43:10 +0200 wenzelm imitate exception ERROR of Isabelle/ML;
Sat, 18 Jun 2011 00:05:29 +0200 wenzelm more robust treatment of partial range restriction;
Fri, 17 Jun 2011 23:18:22 +0200 wenzelm more explicit error message;
Thu, 26 Aug 2010 11:29:43 +0200 wenzelm tuned signature;
Tue, 24 Aug 2010 23:49:07 +0200 wenzelm Text.Range.is_singleton;
Sun, 22 Aug 2010 19:33:01 +0200 wenzelm misc tuning and simplification;
Sun, 22 Aug 2010 18:46:16 +0200 wenzelm renamed Markup_Tree.Node to Text.Info;
Fri, 20 Aug 2010 22:32:15 +0200 wenzelm added Text.Range.- convenience;
Fri, 20 Aug 2010 12:12:28 +0200 wenzelm alternative constructor for Range singularities;
Fri, 20 Aug 2010 11:00:15 +0200 wenzelm further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
Thu, 19 Aug 2010 22:52:00 +0200 wenzelm parameterized type Markup_Tree.Node;
Thu, 19 Aug 2010 22:26:15 +0200 wenzelm added toString methods;
Thu, 19 Aug 2010 22:04:20 +0200 wenzelm misc tuning and simplification;
Thu, 19 Aug 2010 17:37:13 +0200 wenzelm Text.Range: improved handling of singularities;
Wed, 18 Aug 2010 14:02:32 +0200 wenzelm refined notion of Text.Range;
Sun, 15 Aug 2010 23:07:22 +0200 wenzelm some derived operations on Text.Range;
Sun, 15 Aug 2010 22:48:56 +0200 wenzelm specific types Text.Offset and Text.Range;
Sun, 15 Aug 2010 21:42:13 +0200 wenzelm moved Text_Edit to Text.Edit;
less more (0) tip