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