From dc6c9c950700a9707ff1f473ef687f0bda597eb3 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:53:13 +0000 Subject: Gtk check_buttons do have a label git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16687 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/preferences.ml | 18 +----------------- 1 file changed, 1 insertion(+), 17 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index b3ef96fd9..b36e42d4c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -494,24 +494,8 @@ let configure ?(apply=(fun () -> ())) () = let config_editor = let label = "Editor configuration" in let box = GPack.vbox () in - let table = GPack.table - ~row_spacings:5 - ~col_spacings:5 - ~border_width:2 - ~packing:(box#pack ~expand:true) () - in - let row = ref 0 in let gen_button text active = - let button = GButton.check_button - ~packing:(table#attach ~left:0 ~top:!row) () - in - let _ = GMisc.label ~text ~xalign:0. - ~packing:(table#attach ~expand:`X ~left:1 ~top:!row) () - in - let () = incr row in - let () = button#set_active active in - button - in + GButton.check_button ~label:text ~active ~packing:box#pack () in let wrap = gen_button "Dynamic word wrap" current.dynamic_word_wrap in let line = gen_button "Show line number" current.show_line_number in let auto_indent = gen_button "Auto indentation" current.auto_indent in -- cgit v1.2.3