diff options
Diffstat (limited to 'otherlibs/labltk/browser/jg_text.mli')
| -rw-r--r-- | otherlibs/labltk/browser/jg_text.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/jg_text.mli b/otherlibs/labltk/browser/jg_text.mli new file mode 100644 index 0000000000..8b3880eef7 --- /dev/null +++ b/otherlibs/labltk/browser/jg_text.mli @@ -0,0 +1,14 @@ +(* $Id$ *) + +open Widget + +val get_all : text widget -> string +val tag_and_see : + text widget -> + tag:Tk.textTag -> start:Tk.textIndex -> end:Tk.textIndex -> unit +val output : text widget -> buffer:string -> pos:int -> len:int -> unit +val add_scrollbar : text widget -> scrollbar widget +val create_with_scrollbar : + parent:'a widget -> frame widget * text widget * scrollbar widget +val goto_tag : text widget -> tag:string -> unit +val search_string : text widget -> unit |