~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
~check:self#main#tacticsBarMenuItem;
let module Hr = Helm_registry in
- if not(Hr.get_opt_default Hr.get_bool false "matita.tactics_bar") then
+ 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;
(* quit *)
self#setQuitCallback (fun () -> exit 0);
(* log *)
advance ());
(* script monospace font stuff *)
let font =
- Helm_registry.get_opt_default Helm_registry.get
- BuildTimeConf.default_script_font "matita.script_font"
+ Helm_registry.get_opt_default Helm_registry.string
+ ~default:BuildTimeConf.default_script_font "matita.script_font"
in
(* let monospace_tag =
source_buffer#create_tag [`FONT_DESC font]