+let open_contextual_menu_for_selected_terms mmlwidget infos =
+ let button = GdkEvent.Button.button infos in
+ let terms_selected = List.length mmlwidget#get_selections > 0 in
+ if button = 3 then
+ begin
+ let time = GdkEvent.Button.time infos in
+ let menu = GMenu.menu () in
+ let f = new GMenu.factory menu in
+ let whd_menu_item =
+ f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in
+ let reduce_menu_item =
+ f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in
+ let simpl_menu_item =
+ f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in
+ whd_menu_item#misc#set_sensitive terms_selected ;
+ reduce_menu_item#misc#set_sensitive terms_selected ;
+ simpl_menu_item#misc#set_sensitive terms_selected ;
+ menu#popup ~button ~time
+ end ;
+ true
+;;
+