1 files changed, 20 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/shell.mli b/otherlibs/labltk/browser/shell.mli
new file mode 100644
index 0000000000..adea445514
--- /dev/null
+++ b/otherlibs/labltk/browser/shell.mli
@@ -0,0 +1,20 @@
+(* $Id$ *)
+
+(* toplevel shell *)
+
+class shell :
+  textw:Widget.text Widget.widget -> prog:string ->
+  args:string array -> env:string array ->
+  object
+    method alive : bool
+    method kill : unit
+    method interrupt : unit
+    method insert : string -> unit
+    method send : string -> unit
+    method history : [`next|`previous] -> unit
+  end
+
+val kill_all : unit -> unit
+val get_all : unit -> (string * shell) list
+
+val f : prog:string -> title:string -> unit