moved the high level pretty printing setting to a toggle menu item of the View menu...

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ed39ac6525e642912bef5288e35317400032fc0b..b8d20cf3cace3c3557b2c872fe72af18c8ca2e9f 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -1014,6 +1014,10 @@ class gui () =
           | false -> main#toplevel#unfullscreen ())
         ~check:main#fullscreenMenuItem;
       main#fullscreenMenuItem#set_active false;
+      MatitaGtkMisc.toggle_callback
+        ~callback:(fun enabled ->
+          CicMetaSubst.use_low_level_ppterm_in_context := not enabled)
+        ~check:main#formulaePpMenuItem;
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=