wg_Detachable: move out of wg_Command

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 30 deletions

diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index 92ad858f4..9799e8a99 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -6,36 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-class type detachable_signals =
-  object
-    inherit GContainer.container_signals
-    method attached : callback:(GObj.widget -> unit) -> unit
-    method detached : callback:(GObj.widget -> unit) -> unit
-  end
-
-class detachable : ([> Gtk.box] as 'a) Gobject.obj ->
-  object
-    inherit GPack.box_skel
-    val obj : Gtk.box Gobject.obj
-    method connect : detachable_signals
-    method child : GObj.widget
-    method show : unit
-    method hide : unit
-    method visible : bool
-    method title : string
-    method set_title : string -> unit
-
-  end
-
-val detachable :
-  ?title:string ->
-  ?homogeneous:bool ->
-  ?spacing:int ->
-  ?border_width:int ->
-  ?width:int ->
-  ?height:int ->
-  ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> detachable
-
 class command_window : string -> Coq.coqtop ->
   object
     method new_query : ?command:string -> ?term:string -> unit -> unit