diff options
Diffstat (limited to 'otherlibs/labltk/builtin/builtin_text.ml')
| -rw-r--r-- | otherlibs/labltk/builtin/builtin_text.ml | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/otherlibs/labltk/builtin/builtin_text.ml b/otherlibs/labltk/builtin/builtin_text.ml deleted file mode 100644 index b2d69589ba..0000000000 --- a/otherlibs/labltk/builtin/builtin_text.ml +++ /dev/null @@ -1,50 +0,0 @@ -(* Not a string as such, more like a symbol *) - -(* type *) -type textMark = string;; -(* /type *) - -(* type *) -type textTag = string;; -(* /type *) - -##ifdef CAMLTK - -(* type *) -type textModifier = - | CharOffset of int (* tk keyword: +/- Xchars *) - | LineOffset of int (* tk keyword: +/- Xlines *) - | LineStart (* tk keyword: linestart *) - | LineEnd (* tk keyword: lineend *) - | WordStart (* tk keyword: wordstart *) - | WordEnd (* tk keyword: wordend *) -;; -(* /type *) - -(* type *) -type textIndex = - | TextIndex of index * textModifier list - | TextIndexNone -;; -(* /type *) - -##else - -(* type *) -type textModifier = [ - | `Char of int (* tk keyword: +/- Xchars *) - | `Line of int (* tk keyword: +/- Xlines *) - | `Linestart (* tk keyword: linestart *) - | `Lineend (* tk keyword: lineend *) - | `Wordstart (* tk keyword: wordstart *) - | `Wordend (* tk keyword: wordend *) -] -;; -(* /type *) - -(* type *) -type textIndex = text_index * textModifier list -;; -(* /type *) - -##endif |