src/Pure/PIDE/text.scala
Mon, 19 Jun 2017 17:28:48 +0200 wenzelm clarified signature;
Thu, 20 Apr 2017 11:38:42 +0200 wenzelm tuned signature;
Tue, 04 Apr 2017 18:43:58 +0200 wenzelm tuned signature;
Sun, 12 Mar 2017 14:23:38 +0100 wenzelm discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
Wed, 08 Mar 2017 21:41:14 +0100 wenzelm suppress vacuous edits;
Wed, 08 Mar 2017 20:30:05 +0100 wenzelm clarified native Text.Offset versus Text.Length index Int;
Wed, 08 Mar 2017 20:25:57 +0100 wenzelm tuned;
Mon, 06 Mar 2017 17:10:37 +0100 wenzelm tuned;
Sat, 07 Jan 2017 11:22:13 +0100 wenzelm tuned;
Wed, 28 Dec 2016 17:10:09 +0100 wenzelm clarified modules;
Wed, 28 Dec 2016 11:28:31 +0100 wenzelm tuned;
Sat, 10 Dec 2016 17:22:47 +0100 wenzelm clarified output: avoid confusion with line:column notation;
Mon, 24 Oct 2016 12:16:12 +0200 wenzelm discontinued unused / untested distinction of separate PIDE modules;
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;
less more (0) -50 -30 tip