From 0d2ee0feaa643add1be91d1baa19777bd9f68100 Mon Sep 17 00:00:00 2001 From: jnarboux Date: Mon, 26 May 2008 15:51:10 +0000 Subject: transform the toolbar icons for display of information into a Display menu with shortcuts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10992 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 128 ++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 75 insertions(+), 53 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index a29a2519d..5770aeea3 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2641,58 +2641,6 @@ let main files = ~callback:(do_if_active( fun a -> a#insert_command "progress trivial.\n" "trivial.\n" )) ); - - ignore (toolbar#insert_space ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle printing of implicit arguments" - ~text:"Impl" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ()) - ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle printing of coercions" - ~text:"Coer" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ()) - ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle printing of raw matching expressions" - ~text:"Match" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ()) - ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle deactivation of notations" - ~text:"Nota" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ()) - ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle full low-level printing" - ~text:"All" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ()) - ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle printing of existential variable instances" - ~text:"Evars" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ()) - ()); - - ignore (toolbar#insert_toggle_button - ~tooltip:"Toggle printing of universe levels" - ~text:"Univ" - ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) - ~callback:(fun () -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ()) - ()); - ignore (toolbar#insert_space ()); ignore (toolbar#insert_button @@ -2917,6 +2865,80 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ()) in + (* Display menu *) + + let display_menu = factory#add_submenu "_Display" in + let view_factory = new GMenu.factory display_menu + ~accel_path:"/Display/" + ~accel_group + ~accel_modi:[`MOD1;`SHIFT] + in + + let _ = ignore (view_factory#add_check_item + "Toggle printing of _implicit arguments" + ~key:GdkKeysyms._i + ~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Toggle printing of _coercions" + ~key:GdkKeysyms._c + ~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Toggle printing of raw _matching expressions" + ~key:GdkKeysyms._m + ~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Toggle deactivation of _notations" + ~key:GdkKeysyms._n + ~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Toggle _full low-level printing" + ~key:GdkKeysyms._f + ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Toggle printing of _existential variable instances" + ~key:GdkKeysyms._e + ~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Toggle printing of _universe levels" + ~key:GdkKeysyms._u + ~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in + + + (* Unicode *) +(* + let unicode_menu = factory#add_submenu "_Unicode" in + let unicode_factory = new GMenu.factory unicode_menu + ~accel_path:"/Unicode/" + ~accel_group + ~accel_modi:[] + in + let logic_symbols_menu = unicode_factory#add_submenu "Math operators" in + let logic_factory = new GMenu.factory logic_symbols_menu + ~accel_path:"/Unicode/Math operators" + ~accel_group + ~accel_modi:[] + in + let new_unicode_item s = ignore ( + logic_factory#add_item s + ~callback:(fun () -> + let v = get_current_view () in + ignore (v.view#buffer#insert_interactive s))) + in + + for i = 0x2200 to 0x22FF do + List.iter new_unicode_item [Glib.Utf8.from_unichar i]; + + done; + +*) + + (* Externals *) let externals_menu = factory#add_submenu "_Compile" in let externals_factory = new GMenu.factory externals_menu @@ -3147,7 +3169,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let nb = notebook () in let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in - let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in + let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in let sw2 = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC -- cgit v1.2.3