contribs: some improvements

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index cc8a885e8837a93e7800fd5dbe73886de1d8340d..a9faa592e8de974b5ce3192a81eacf22f556ac0c 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -1012,16 +1012,27 @@ class gui () =
         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
       then 
         main#tacticsBarMenuItem#set_active false;
-      MatitaGtkMisc.toggle_callback 
+      MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
           | true -> main#toplevel#fullscreen () 
-          | false -> main#toplevel#unfullscreen ())
-        ~check:main#fullscreenMenuItem;
+          | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
-      MatitaGtkMisc.toggle_callback
+      MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
+        ~callback:(function
+          | true ->
+              CicNotation.set_active_notations
+                (List.map fst (CicNotation.get_all_notations ()))
+          | false ->
+              CicNotation.set_active_notations []);
+      MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
+        ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+      MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
-          CicMetaSubst.use_low_level_ppterm_in_context := not enabled)
-        ~check:main#formulaePpMenuItem;
+          Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
+      if not (Helm_registry.has "matita.paste_unicode_as_tex") then
+        Helm_registry.set_bool "matita.paste_unicode_as_tex" true;
+      main#unicodeAsTexMenuItem#set_active
+        (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=