From: Stefano Zacchiroli Date: Fri, 9 Feb 2007 13:29:08 +0000 (+0000) Subject: moved the high level pretty printing setting to a toggle menu item of the View menu... X-Git-Tag: 0.4.95@7852~608 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a1b43d009dc6eb9a64e35e08fccbef4313140b8;p=helm.git moved the high level pretty printing setting to a toggle menu item of the View menu (with CTRL-P shortcut) --- diff --git a/matita/matita.glade b/matita/matita.glade index b8ae58347..8cc437f39 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -1081,7 +1081,7 @@ - + True gtk-new 1 @@ -1102,7 +1102,7 @@ - + True gtk-open 1 @@ -1123,7 +1123,7 @@ - + True gtk-save 1 @@ -1139,12 +1139,12 @@ True - Save _As ... + Save _as ... True - + True gtk-save-as 1 @@ -1165,7 +1165,7 @@ - + True gtk-execute 1 @@ -1192,7 +1192,7 @@ - + True gtk-quit 1 @@ -1227,7 +1227,7 @@ - + True gtk-undo 1 @@ -1249,7 +1249,7 @@ - + True gtk-redo 1 @@ -1276,7 +1276,7 @@ - + True gtk-cut 1 @@ -1297,7 +1297,7 @@ - + True gtk-copy 1 @@ -1318,7 +1318,7 @@ - + True gtk-paste 1 @@ -1346,7 +1346,7 @@ True - + True gtk-delete 1 @@ -1382,12 +1382,12 @@ True - _Find & Replace ... + _Find & replace ... True - + True gtk-find-and-replace 1 @@ -1418,7 +1418,7 @@ True - Edit with E_xternal Editor + Edit with e_xternal editor True @@ -1509,7 +1509,7 @@ True - Show _Tactics Bar + Show _tactics bar True True @@ -1519,7 +1519,7 @@ True - New Cic _Browser + New CIC _browser True @@ -1550,13 +1550,12 @@ True - Zoom _In + Zoom _in True - - + True gtk-zoom-in 1 @@ -1572,13 +1571,12 @@ True - Zoom _Out + Zoom _out True - - + True gtk-zoom-out 1 @@ -1594,12 +1592,12 @@ True - _Normal Size + _Normal size True - + True gtk-zoom-100 1 @@ -1611,6 +1609,22 @@ + + + + True + + + + + + True + Pretty print formulae + True + True + + + @@ -1652,7 +1666,7 @@ - + True gtk-help 1 @@ -1672,7 +1686,7 @@ True - + True gtk-about 1 @@ -4423,238 +4437,6 @@ - - True - window1 - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - True - False - - - - True - False - 0 - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - True - Restart - True - GTK_RELIEF_NONE - True - - - - True - gtk-goto-top - 4 - 0.5 - 0.5 - 0 - 0 - - - - - - - False - False - - - - - - True - True - True - False - - - - True - Retract 1 phrase - True - GTK_RELIEF_NONE - True - - - - True - gtk-go-up - 4 - 0.5 - 0.5 - 0 - 0 - - - - - - - False - False - - - - - - True - True - True - False - - - - True - Execute until point - True - GTK_RELIEF_NONE - True - - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - - - - - - False - False - - - - - - True - True - True - False - - - - True - Execute 1 phrase - True - GTK_RELIEF_NONE - True - - - - True - gtk-go-down - 4 - 0.5 - 0.5 - 0 - 0 - - - - - - - False - False - - - - - - True - True - True - False - - - - True - Execute all - True - GTK_RELIEF_NONE - True - - - - True - gtk-goto-bottom - 4 - 0.5 - 0.5 - 0 - 0 - - - - - - - False - False - - - - - 0 - True - True - - - - - - True - gtk-cancel - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - 450 400 diff --git a/matita/matita.ml b/matita/matita.ml index dc0aa579d..ce9280dcd 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -214,10 +214,12 @@ let _ = ); addDebugSeparator (); *) +(* ZACK: moved to a check box menu item in the View menu addDebugItem "disable high level pretty printer" (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true); addDebugItem "enable high level pretty printer" (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false); +*) addDebugItem "disable all (pretty printing) notations" (fun _ -> CicNotation.set_active_notations []); addDebugItem "enable all (pretty printing) notations" diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index ed39ac652..b8d20cf3c 100644 --- 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 :=