- moved back the high level pp toggle to the debug menu
<accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image979">
+ <widget class="GtkImage" id="image1013">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image980">
+ <widget class="GtkImage" id="image1014">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image981">
+ <widget class="GtkImage" id="image1015">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image982">
+ <widget class="GtkImage" id="image1016">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image983">
+ <widget class="GtkImage" id="image1017">
<property name="visible">True</property>
<property name="stock">gtk-execute</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-execute</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image984">
+ <widget class="GtkImage" id="image1018">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image985">
+ <widget class="GtkImage" id="image1019">
<property name="visible">True</property>
<property name="stock">gtk-undo</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-undo</property>
<property name="icon_size">1</property>
<accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image986">
+ <widget class="GtkImage" id="image1020">
<property name="visible">True</property>
<property name="stock">gtk-redo</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-redo</property>
<property name="icon_size">1</property>
<accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image987">
+ <widget class="GtkImage" id="image1021">
<property name="visible">True</property>
<property name="stock">gtk-cut</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-cut</property>
<property name="icon_size">1</property>
<accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image988">
+ <widget class="GtkImage" id="image1022">
<property name="visible">True</property>
<property name="stock">gtk-copy</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-copy</property>
<property name="icon_size">1</property>
<accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image989">
+ <widget class="GtkImage" id="image1023">
<property name="visible">True</property>
<property name="stock">gtk-paste</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-paste</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image990">
+ <widget class="GtkImage" id="image1024">
<property name="visible">True</property>
<property name="stock">gtk-delete</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-delete</property>
<property name="icon_size">1</property>
<accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image991">
+ <widget class="GtkImage" id="image1025">
<property name="visible">True</property>
<property name="stock">gtk-find-and-replace</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-find-and-replace</property>
<property name="icon_size">1</property>
<accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image992">
+ <widget class="GtkImage" id="image1026">
<property name="visible">True</property>
<property name="stock">gtk-zoom-in</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-zoom-in</property>
<property name="icon_size">1</property>
<accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image993">
+ <widget class="GtkImage" id="image1027">
<property name="visible">True</property>
<property name="stock">gtk-zoom-out</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-zoom-out</property>
<property name="icon_size">1</property>
<accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
<accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image994">
+ <widget class="GtkImage" id="image1028">
<property name="visible">True</property>
<property name="stock">gtk-zoom-100</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-zoom-100</property>
<property name="icon_size">1</property>
- <widget class="GtkCheckMenuItem" id="formulaePpMenuItem">
+ <widget class="GtkCheckMenuItem" id="ppNotationMenuItem">
<property name="visible">True</property>
<property name="visible">True</property>
- <property name="label" translatable="yes">Pretty print formulae</property>
+ <property name="label" translatable="yes">Pretty print notation</property>
+ <property name="use_underline">True</property>
+ <property name="active">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkCheckMenuItem" id="hideCoercionsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Hide coercions</property>
<property name="use_underline">True</property>
<property name="active">True</property>
<property name="use_underline">True</property>
<property name="active">True</property>
- <accelerator key="p" modifiers="GDK_CONTROL_MASK" signal="activate"/>
</widget>
</child>
</widget>
</widget>
</child>
</widget>
<accelerator key="F1" modifiers="0" signal="activate"/>
<child internal-child="image">
<accelerator key="F1" modifiers="0" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image995">
+ <widget class="GtkImage" id="image1029">
<property name="visible">True</property>
<property name="stock">gtk-help</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-help</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image996">
+ <widget class="GtkImage" id="image1030">
<property name="visible">True</property>
<property name="stock">gtk-about</property>
<property name="icon_size">1</property>
<property name="visible">True</property>
<property name="stock">gtk-about</property>
<property name="icon_size">1</property>
);
addDebugSeparator ();
*)
);
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 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 ())));
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 ();
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 "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));
addDebugItem "show coercions graph" (fun _ ->
let c = MatitaMathView.cicBrowser () in
c#load (`About `Coercions));
| false -> main#toplevel#unfullscreen ())
~check:main#fullscreenMenuItem;
main#fullscreenMenuItem#set_active false;
| 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 :=
(* log *)
HLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=