added comments, fixed history, added loadList to browser

[helm.git] / helm / matita / matitaGtkMisc.ml

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 274ee123a2a9ba48e38d5bd811a7317f16ed0586..0301b31f2e3981a02aad48493943af7a04c03223 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -39,6 +39,9 @@ let wrap_callback f () =
 let connect_button (button: #GButton.button) callback =
   ignore (button#connect#clicked (wrap_callback callback))
 
+let connect_toggle_button (button: #GButton.toggle_button) callback =
+  ignore (button#connect#toggled (wrap_callback callback))
+
 let connect_menu_item (menu_item: #GMenu.menu_item) callback =
   ignore (menu_item#connect#activate (wrap_callback callback))