- connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None)));
- (* quit *)
- self#setQuitCallback (fun () -> exit 0);
+ connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
+ MatitaGtkMisc.toggle_widget_visibility
+ ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
+ ~check:self#main#tacticsBarMenuItem;
+ let module Hr = Helm_registry in
+ if
+ not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
+ then
+ self#main#tacticsBarMenuItem#set_active false;
+ MatitaGtkMisc.toggle_callback
+ ~callback:(function
+ | true -> self#main#toplevel#fullscreen ()
+ | false -> self#main#toplevel#unfullscreen ())
+ ~check:self#main#fullscreenMenuItem;
+ self#main#fullscreenMenuItem#set_active false;