| 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
|