| Mon, 19 Jun 2017 17:28:48 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 11:38:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 18:43:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 12 Mar 2017 14:23:38 +0100 |
wenzelm |
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 21:41:14 +0100 |
wenzelm |
suppress vacuous edits;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 20:30:05 +0100 |
wenzelm |
clarified native Text.Offset versus Text.Length index Int;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 20:25:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2017 17:10:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 11:22:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 17:10:09 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 11:28:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Dec 2016 17:22:47 +0100 |
wenzelm |
clarified output: avoid confusion with line:column notation;
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 12:16:12 +0200 |
wenzelm |
discontinued unused / untested distinction of separate PIDE modules;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:49:51 +0200 |
wenzelm |
some structure matching, based on line token iterators;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:46:20 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 16:20:07 +0200 |
wenzelm |
more explicit treatment of cleared nodes (removal is implicit);
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:34:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 16:07:02 +0200 |
wenzelm |
avoid data redundancy;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 15:12:54 +0200 |
wenzelm |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 21:16:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 11:39:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Aug 2012 21:48:09 +0200 |
wenzelm |
tuned import;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 17:13:25 +0100 |
wenzelm |
prefer final ADTs -- prevent ooddities;
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 17:08:32 +0100 |
wenzelm |
approximate Perspective.full within the bounds of the JVM;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 14:34:42 +0100 |
wenzelm |
clarified partial restrict operation;
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 21:29:53 +0100 |
wenzelm |
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:18:19 +0100 |
wenzelm |
explicit indication of modules for independent Scala library;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 12 Nov 2011 17:52:28 +0100 |
wenzelm |
more precise type;
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 14:24:38 +0100 |
wenzelm |
prefer statically typed Text.Markup;
|
file |
diff |
annotate
|
| Sat, 22 Oct 2011 23:29:44 +0200 |
wenzelm |
class Text.Edit as abstract datatype;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 11:41:48 +0200 |
wenzelm |
slightly more abstract Command.Perspective;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 11:27:37 +0200 |
wenzelm |
slightly more abstract Text.Perspective;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 21:42:02 +0200 |
wenzelm |
some support for editor perspective;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 16:12:23 +0200 |
wenzelm |
added official Text.Range.Ordering;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 12:56:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 13:43:10 +0200 |
wenzelm |
imitate exception ERROR of Isabelle/ML;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2011 00:05:29 +0200 |
wenzelm |
more robust treatment of partial range restriction;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2011 23:18:22 +0200 |
wenzelm |
more explicit error message;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 11:29:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 23:49:07 +0200 |
wenzelm |
Text.Range.is_singleton;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 19:33:01 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 18:46:16 +0200 |
wenzelm |
renamed Markup_Tree.Node to Text.Info;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 22:32:15 +0200 |
wenzelm |
added Text.Range.- convenience;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 12:12:28 +0200 |
wenzelm |
alternative constructor for Range singularities;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 22:52:00 +0200 |
wenzelm |
parameterized type Markup_Tree.Node;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 22:26:15 +0200 |
wenzelm |
added toString methods;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 22:04:20 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 17:37:13 +0200 |
wenzelm |
Text.Range: improved handling of singularities;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 14:02:32 +0200 |
wenzelm |
refined notion of Text.Range;
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 23:07:22 +0200 |
wenzelm |
some derived operations on Text.Range;
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 22:48:56 +0200 |
wenzelm |
specific types Text.Offset and Text.Range;
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 21:42:13 +0200 |
wenzelm |
moved Text_Edit to Text.Edit;
|
file |
diff |
annotate
| base
|