in
tooltip#set_tip ~text (button :> GObj.widget);
ignore(button#connect#clicked
- (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
+ (fun _ ->
+ let menu = GMenu.menu () in
+ let follow = GMenu.menu_item ~label:"Follow" () in
+ let prune = GMenu.menu_item ~label:"Prune" () in
+ ignore (follow#connect#activate
+ (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
+ ignore (prune#connect#activate
+ (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id));
+ menu#append follow;
+ menu#append prune;
+ menu#popup 0 (GtkMain.Main.get_current_event_time ())));
button
;;
let cell_of_goal height win_width context goal =
;;
let elems_to_rows height context win_width (table : GPack.table) (or_list) =
- let height = height / (List.length or_list) in
+ let height = height / ((List.length or_list) + 1) in
let _ =
List.fold_left
(fun position (goal_id, goal, grey, depth, candidates) ->
Auto.step ();
win#toplevel#destroy ();
GMain.Main.quit ()));
+ ignore(win#toplevel#event#connect#delete
+ (fun _ ->
+ Auto.pause false;
+ Auto.step ();
+ win#toplevel#destroy ();
+ GMain.Main.quit ();true));
let redraw_callback _ = fill_win win elems;true in
let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
ignore(win#buttonPAUSE#connect#clicked