From: Stefano Zacchiroli Date: Fri, 9 Feb 2007 15:18:08 +0000 (+0000) Subject: - moved to the view menu toggles for coercion hiding and notation pp X-Git-Tag: make_still_working~6463 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c55d66bd91cc2e12daf076c4bd050ce34029854f;p=helm.git - moved to the view menu toggles for coercion hiding and notation pp - moved back the high level pp toggle to the debug menu --- diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 8cc437f39..4b3378513 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/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 @@ -1144,7 +1144,7 @@ - + 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 @@ -1387,7 +1387,7 @@ - + True gtk-find-and-replace 1 @@ -1555,7 +1555,7 @@ - + True gtk-zoom-in 1 @@ -1576,7 +1576,7 @@ - + True gtk-zoom-out 1 @@ -1597,7 +1597,7 @@ - + True gtk-zoom-100 1 @@ -1617,12 +1617,20 @@ - + True - Pretty print formulae + Pretty print notation + True + True + + + + + + True + Hide coercions True True - @@ -1666,7 +1674,7 @@ - + True gtk-help 1 @@ -1686,7 +1694,7 @@ True - + True gtk-about 1 diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index ce9280dcd..a23558aa8 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -214,28 +214,30 @@ 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); -*) +(* ZACK moved to the View menu addDebugItem "disable all (pretty printing) notations" (fun _ -> CicNotation.set_active_notations []); addDebugItem "enable all (pretty printing) notations" (fun _ -> CicNotation.set_active_notations (List.map fst (CicNotation.get_all_notations ()))); +*) addDebugSeparator (); addDebugItem "enable multiple disambiguation passes (default)" (fun _ -> GrafiteDisambiguator.only_one_pass := false); addDebugItem "enable only one disambiguation pass" (fun _ -> GrafiteDisambiguator.only_one_pass := true); addDebugSeparator (); +(* ZACK moved to the View menu addDebugItem "enable coercions hiding" (fun _ -> Acic2content.hide_coercions := true); addDebugItem "disable coercions hiding" (fun _ -> Acic2content.hide_coercions := false); +*) addDebugItem "show coercions graph" (fun _ -> let c = MatitaMathView.cicBrowser () in c#load (`About `Coercions)); diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index cc8a885e8..f40efe867 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1018,10 +1018,15 @@ 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; + 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); (* log *) HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler :=