icons in tool box

src/ide/gconfig.ml

@@ -189,6 +189,7 @@ let iconname_directory = "folder32"
 let iconname_file = "file32"
 let iconname_prover = "wizard32"
 let iconname_transf = "cutb32"
+let iconname_editor = "edit32"
 
 let image_default = ref (image ~size:20 iconname_default)
 let image_scheduled = ref !image_default
@@ -204,6 +205,7 @@ let image_directory = ref !image_default
 let image_file = ref !image_default
 let image_prover = ref !image_default
 let image_transf = ref !image_default
+let image_editor = ref !image_default
 
 let resize_images size =
   image_default := image ~size iconname_default;
@@ -220,6 +222,7 @@ let resize_images size =
   image_file := image ~size iconname_file;
   image_prover := image ~size iconname_prover;
   image_transf := image ~size iconname_transf;
+  image_editor := image ~size iconname_editor;
   ()
 
 let () =

src/ide/gconfig.mli

@@ -47,6 +47,7 @@ val image_directory : GdkPixbuf.pixbuf ref
 val image_file : GdkPixbuf.pixbuf ref
 val image_prover : GdkPixbuf.pixbuf ref
 val image_transf : GdkPixbuf.pixbuf ref
+val image_editor : GdkPixbuf.pixbuf ref
 
 (* status icons *)
 val image_scheduled : GdkPixbuf.pixbuf ref

src/ide/gdbmain.ml

@@ -1328,6 +1328,8 @@ let () =
              ()
          in
          let b = GButton.button ~packing:tools_box#add ~label:n () in
+         let i = GMisc.image ~pixbuf:(!image_prover) ()in
+         let () = b#set_image i#coerce in
          let (_ : GtkSignal.id) =
            b#connect#pressed 
              ~callback:(fun () -> prover_on_selected_goals p)
@@ -1349,6 +1351,8 @@ let () =
 
 let () =
   let b = GButton.button ~packing:others_box#add ~label:"Split" () in
+  let i = GMisc.image ~pixbuf:(!image_transf) () in
+  let () = b#set_image i#coerce in
   let (_ : GtkSignal.id) =
     b#connect#pressed ~callback:split_selected_goals
   in ()
@@ -1612,6 +1616,8 @@ let () =
 
 let () =
   let b = GButton.button ~packing:others_box#add ~label:"Edit" () in
+  let i = GMisc.image ~pixbuf:(!image_editor) () in
+  let () = b#set_image i#coerce in
   let (_ : GtkSignal.id) =
     b#connect#pressed ~callback:edit_current_proof
   in ()