From aa357d601d440a2e22de61299e0f87e79bed27fd Mon Sep 17 00:00:00 2001 From: marche Date: Thu, 4 Dec 2003 15:31:52 +0000 Subject: changement menu et toolbar git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5065 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/command_windows.ml | 61 +++++++++++- ide/coq.ml | 13 ++- ide/coqide.ml | 248 ++++++++++++++++++++++++++++--------------------- ide/preferences.ml | 46 +++++---- ide/preferences.mli | 2 + 5 files changed, 239 insertions(+), 131 deletions(-) (limited to 'ide') diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 3f773b79c..444495ee1 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -30,11 +30,34 @@ class command_window () = in let accel_group = GtkData.AccelGroup.create () in let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in +(* let menubar = GMenu.menu_bar ~packing:vbox#pack () in +*) +(* + let handle = GBin.handle_box + ~show:true + ~handle_position:`LEFT + ~snap_edge:`LEFT + ~packing:vbox#pack + () + in +*) + let toolbar = GButton.toolbar + ~orientation:`HORIZONTAL + ~style:`ICONS + ~tooltips:true + ~packing:(vbox#pack + ~expand:false + ~fill:false) + () + in +(* let factory = new GMenu.factory menubar in +*) +(* let accel_group = factory#accel_group in - +*) let notebook = GPack.notebook ~scrollable:true ~packing:(vbox#pack ~expand:true @@ -42,18 +65,52 @@ class command_window () = ) () in +(* let hide_menu = factory#add_item "_Hide Window" ~callback:window#misc#hide +*) + let _ = + toolbar#insert_button + ~tooltip:"Hide Window" + ~text:"Hide Window" + ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `CLOSE) + ~callback:window#misc#hide + () in +(* let new_page_menu = factory#add_item "_New Page" in +*) + let new_page_menu = + toolbar#insert_button + ~tooltip:"New Page" + ~text:"New Page" + ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `NEW) +(* + ~callback:window#misc#hide +*) + () + in + +(* let kill_page_menu = factory#add_item "_Kill Page" ~callback: (fun () -> notebook#remove_page notebook#current_page) in +*) + let kill_page_menu = + toolbar#insert_button + ~tooltip:"Kill Page" + ~text:"Kill Page" + ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `DELETE) + ~callback:(fun () -> notebook#remove_page notebook#current_page) + () + in object(self) val window = window +(* val menubar = menubar +*) val new_page_menu = new_page_menu val notebook = notebook method window = window @@ -122,7 +179,7 @@ object(self) self#window#present () initializer - ignore (new_page_menu#connect#activate self#new_command); + ignore (new_page_menu#connect#clicked self#new_command); ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true)); end diff --git a/ide/coq.ml b/ide/coq.ml index 1f0efbe71..0de38431a 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -48,13 +48,18 @@ let init () = let i = ref 0 let version () = - Printf.sprintf "The Coq Proof Assistant, version %s (%s)\nConfigured on %s\nThis is the %s version (%s is the best one) for architecture %s on system %s -Gtk version is %s" + Printf.sprintf + "The Coq Proof Assistant, version %s (%s)\ + \nConfigured on %s\ + \nArchitecture %s running %s operating system\ + \nGtk version is %s\ + \nThis is the %s version (%s is the best one for this architecture and OS)\ + \n" Coq_config.version Coq_config.date Coq_config.compile_date - (if Mltop.get () = Mltop.Native then "native" else "byte") - (if Coq_config.best="opt" then "native" else "byte") Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) + (if Mltop.get () = Mltop.Native then "native" else "bytecode") + (if Coq_config.best="opt" then "native" else "bytecode") let is_in_coq_lib dir = prerr_endline ("Is it a coq theory ? : "^dir); diff --git a/ide/coqide.ml b/ide/coqide.ml index d4bd7def2..ea1c88958 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1369,7 +1369,7 @@ Please restart and report NOW."; let set_goal i (s,t) = let gnb = string_of_int i in let s = gnb ^":"^s in - let t' = gnb ^": Progress "^t in + let t' = gnb ^": progress "^t in let t'' = gnb ^": "^t in c#set ("Goal "^gnb) @@ -1381,7 +1381,7 @@ Please restart and report NOW."; c#set "Goal 1" s - (fun () -> try_interptac ("Progress "^t)) + (fun () -> try_interptac ("progress "^t)) (fun () -> self#insert_command t t) in begin match current_gls with @@ -1723,6 +1723,7 @@ let main files = let menubar = GMenu.menu_bar ~packing:vbox#pack () in (* Tearable Toolbar *) +(* let handle = GBin.handle_box ~show:!current.show_toolbar ~handle_position:`LEFT @@ -1730,15 +1731,21 @@ let main files = ~packing:vbox#pack () in +*) let toolbar = GButton.toolbar ~orientation:`HORIZONTAL - ~style:`BOTH + ~style:`ICONS ~tooltips:true - ~packing:handle#add + ~packing:(* handle#add *) + (vbox#pack ~expand:false ~fill:false) () in +(* show_toolbar := (fun b -> if b then handle#misc#show () else handle#misc#hide ()); +*) + show_toolbar := + (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ()); let factory = new GMenu.factory ~accel_path:"/" menubar in let accel_group = factory#accel_group in @@ -2003,6 +2010,7 @@ let main files = *) (* File/Quit Menu *) let quit_f () = + save_pref(); if has_something_to_save () then match (GToolbox.question_box ~title:"Quit" ~buttons:["Save Named Buffers and Quit"; @@ -2057,13 +2065,6 @@ let main files = with _ -> prerr_endline "EMIT PASTE FAILED"))); ignore (edit_f#add_separator ()); - ignore(edit_f#add_item "Complete" ~key:GdkKeysyms._slash ~callback: - (do_if_not_computing - (fun () -> - ignore ( - let av = out_some ((get_current_view()).analyzed_view) in - av#complete_at_offset (av#get_insert)#offset - )))); (* let toggle_auto_complete_i = @@ -2089,6 +2090,7 @@ let main files = let search_ib = edit_f#add_item "Search _backward" ~key:GdkKeysyms._less in +(* let complete_i = edit_f#add_item "_Complete" ~key:GdkKeysyms._comma ~callback: @@ -2101,7 +2103,16 @@ let main files = )) in complete_i#misc#set_state `INSENSITIVE; +*) + ignore(edit_f#add_item "Complete" ~key:GdkKeysyms._slash ~callback: + (do_if_not_computing + (fun () -> + ignore ( + let av = out_some ((get_current_view()).analyzed_view) in + av#complete_at_offset (av#get_insert)#offset + )))); + to_do_on_page_switch := (fun i -> prerr_endline ("Switching to tab "^(string_of_int i)); @@ -2109,6 +2120,54 @@ let main files = read_only_i#set_active v#read_only )::!to_do_on_page_switch; + + ignore(edit_f#add_separator ()); + (* Preferences *) + let reset_revert_timer () = + disconnect_revert_timer (); + if !current.global_auto_revert then + revert_timer := Some + (GMain.Timeout.add ~ms:!current.global_auto_revert_delay + ~callback: + (fun () -> + do_if_not_computing (fun () -> revert_f ()) (); + true)) + in reset_revert_timer (); (* to enable statup preferences timer *) + + let auto_save_f () = + Vector.iter + (function + {view = view ; analyzed_view = Some av} as full -> + (try + av#auto_save + with _ -> ()) + | _ -> () + ) + input_views + in + + let reset_auto_save_timer () = + disconnect_auto_save_timer (); + if !current.auto_save then + auto_save_timer := Some + (GMain.Timeout.add ~ms:!current.auto_save_delay + ~callback: + (fun () -> + do_if_not_computing (fun () -> auto_save_f ()) (); + true)) + in reset_auto_save_timer (); (* to enable statup preferences timer *) + + + let edit_prefs_m = + edit_f#add_item "_Preferences" + ~callback:(fun () -> configure ();reset_revert_timer ()) + in +(* + let save_prefs_m = + configuration_factory#add_item "_Save preferences" + ~callback:(fun () -> save_pref ()) + in +*) (* Navigation Menu *) let navigation_menu = factory#add_submenu "_Navigation" in let navigation_factory = @@ -2144,19 +2203,19 @@ let main files = ()) in add_to_menu_toolbar "_Interrupt" - ~tooltip:"Interrupt" + ~tooltip:"Interrupt computations" ~key:GdkKeysyms._Break ~callback:break `STOP ; add_to_menu_toolbar "_Forward" - ~tooltip:"Forward" + ~tooltip:"Forward one command" ~key:GdkKeysyms._Down ~callback:(do_or_activate (fun a -> a#process_next_phrase true true)) `GO_DOWN; add_to_menu_toolbar "_Backward" - ~tooltip:"Backward" + ~tooltip:"Backward one command" ~key:GdkKeysyms._Up ~callback:(do_or_activate (fun a -> a#undo_last_step)) `GO_UP; @@ -2176,19 +2235,19 @@ let main files = *) add_to_menu_toolbar "_Go to" - ~tooltip:"Go to" + ~tooltip:"Go to cursor" ~key:GdkKeysyms._Right ~callback:(do_or_activate (fun a-> a#go_to_insert)) - `GOTO_LAST; + `JUMP_TO; add_to_menu_toolbar "_Start" - ~tooltip:"Start" + ~tooltip:"Go to start" ~key:GdkKeysyms._Home ~callback:(do_or_activate (fun a -> a#reset_initial)) `GOTO_TOP; add_to_menu_toolbar "_End" - ~tooltip:"End" + ~tooltip:"Go to end" ~key:GdkKeysyms._End ~callback:(do_or_activate (fun a -> a#process_until_end_or_error)) `GOTO_BOTTOM; @@ -2208,53 +2267,57 @@ let main files = in let do_if_active f = do_if_not_computing (do_if_active_raw f) in - ignore (tactics_factory#add_item "_Blaster" + let blaster_i = + tactics_factory#add_item "_Blaster" ~key:GdkKeysyms._b ~callback: (do_if_active_raw (fun a -> a#blaster ())) (* Custom locking mechanism! *) - ) - ; - - ignore (tactics_factory#add_item "_Auto" + in + blaster_i#misc#set_state `INSENSITIVE; + + ignore (tactics_factory#add_item "_auto" ~key:GdkKeysyms._a - ~callback:(do_if_active (fun a -> a#insert_command "Progress Auto.\n" "Auto.\n")) + ~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n")) ); - ignore (tactics_factory#add_item "_Auto with *" + ignore (tactics_factory#add_item "_auto with *" ~key:GdkKeysyms._asterisk ~callback:(do_if_active (fun a -> a#insert_command - "Progress Auto with *.\n" - "Auto with *.\n"))); - ignore (tactics_factory#add_item "_EAuto" + "progress auto with *.\n" + "auto with *.\n"))); + ignore (tactics_factory#add_item "_eauto" ~key:GdkKeysyms._e ~callback:(do_if_active (fun a -> a#insert_command - "Progress EAuto.\n" - "EAuto.\n")) + "progress eauto.\n" + "eauto.\n")) ); - ignore (tactics_factory#add_item "_EAuto with *" + ignore (tactics_factory#add_item "_eauto with *" ~key:GdkKeysyms._ampersand ~callback:(do_if_active (fun a -> a#insert_command - "Progress EAuto with *.\n" - "EAuto with *.\n")) + "progress eauto with *.\n" + "eauto with *.\n")) ); - ignore (tactics_factory#add_item "_Intuition" + ignore (tactics_factory#add_item "_intuition" ~key:GdkKeysyms._i - ~callback:(do_if_active (fun a -> a#insert_command "Progress Intuition.\n" "Intuition.\n")) + ~callback:(do_if_active (fun a -> a#insert_command + "progress intuition.\n" + "intuition.\n")) ); - ignore (tactics_factory#add_item "_Omega" + ignore (tactics_factory#add_item "_omega" ~key:GdkKeysyms._o - ~callback:(do_if_active (fun a -> a#insert_command "Omega.\n" "Omega.\n")) + ~callback:(do_if_active (fun a -> a#insert_command + "omega.\n" "omega.\n")) ); - ignore (tactics_factory#add_item "_Simpl" + ignore (tactics_factory#add_item "_simpl" ~key:GdkKeysyms._s - ~callback:(do_if_active (fun a -> a#insert_command "Progress Simpl.\n" "Simpl.\n" )) + ~callback:(do_if_active (fun a -> a#insert_command "progress simpl.\n" "simpl.\n" )) ); - ignore (tactics_factory#add_item "_Tauto" + ignore (tactics_factory#add_item "_tauto" ~key:GdkKeysyms._p - ~callback:(do_if_active (fun a -> a#insert_command "Tauto.\n" "Tauto.\n" )) + ~callback:(do_if_active (fun a -> a#insert_command "tauto.\n" "tauto.\n" )) ); - ignore (tactics_factory#add_item "_Trivial" + ignore (tactics_factory#add_item "_trivial" ~key:GdkKeysyms._v - ~callback:(do_if_active( fun a -> a#insert_command "Progress Trivial.\n" "Trivial.\n" )) + ~callback:(do_if_active( fun a -> a#insert_command "progress trivial.\n" "trivial.\n" )) ); @@ -2358,6 +2421,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ignore (view#buffer#insert_interactive text)))) in ignore (templates_factory#add_separator ()); +(* List.iter (add_simple_template templates_factory) [ "_Auto", "Auto "; "_Auto with *", "Auto with * "; @@ -2370,6 +2434,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); "Tri_vial", "Trivial "; ]; ignore (templates_factory#add_separator ()); +*) List.iter (fun l -> match l with @@ -2400,12 +2465,6 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in (* Command/Show commands *) - let queries_show_m = queries_factory#add_item - "_Show Query Window" - ~key:GdkKeysyms._F12 - ~callback:(Command_windows.command_window ()) - #window#present - in let _ = queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2 ~callback:(fun () -> let term = get_current_word () in @@ -2432,9 +2491,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in (* Externals *) - let externals_menu = factory#add_submenu "_Externals" in + let externals_menu = factory#add_submenu "_Compile" in let externals_factory = new GMenu.factory externals_menu - ~accel_path:"/Externals/" + ~accel_path:"/Compile/" ~accel_group in (* Command/Compile Menu *) @@ -2460,7 +2519,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); av#insert_message res end in - let compile_m = externals_factory#add_item "_Compile" ~callback:compile_f in + let compile_m = externals_factory#add_item "_Compile Buffer" ~callback:compile_f in (* Command/Make Menu *) let make_f () = @@ -2481,56 +2540,29 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); !flash_info (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in - let _ = externals_factory#add_item "_Make Makefile" ~callback:coq_makefile_f + let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f in - (* Configuration Menu *) - let reset_revert_timer () = - disconnect_revert_timer (); - if !current.global_auto_revert then - revert_timer := Some - (GMain.Timeout.add ~ms:!current.global_auto_revert_delay - ~callback: - (fun () -> - do_if_not_computing (fun () -> revert_f ()) (); - true)) - in reset_revert_timer (); (* to enable statup preferences timer *) - - let auto_save_f () = - Vector.iter - (function - {view = view ; analyzed_view = Some av} as full -> - (try - av#auto_save - with _ -> ()) - | _ -> () - ) - input_views + (* Windows Menu *) + let configuration_menu = factory#add_submenu "_Windows" in + let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"/Windows" ~accel_group in - - let reset_auto_save_timer () = - disconnect_auto_save_timer (); - if !current.auto_save then - auto_save_timer := Some - (GMain.Timeout.add ~ms:!current.auto_save_delay - ~callback: - (fun () -> - do_if_not_computing (fun () -> auto_save_f ()) (); - true)) - in reset_auto_save_timer (); (* to enable statup preferences timer *) - - let configuration_menu = factory#add_submenu "Confi_guration" in - let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"/Configuration" ~accel_group - in - let edit_prefs_m = - configuration_factory#add_item "Edit _preferences" - ~callback:(fun () -> configure ();reset_revert_timer ()) - in - let save_prefs_m = - configuration_factory#add_item "_Save preferences" - ~callback:(fun () -> save_pref ()) + let queries_show_m = + configuration_factory#add_item + "Show _Query Window" + (* + ~key:GdkKeysyms._F12 + *) + ~callback:(Command_windows.command_window ())#window#present + in + let toolbar_show_m = + configuration_factory#add_item + "Show/Hide _Toolbar" + ~callback:(fun () -> + !current.show_toolbar <- not !current.show_toolbar; + !show_toolbar !current.show_toolbar) in let detach_menu = configuration_factory#add_item - "_Detach Scripting Window" + "Detach _Script Window" ~callback: (do_if_not_computing (fun () -> @@ -2548,7 +2580,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); )) in let detach_current_view = configuration_factory#add_item - "De_tach View" + "Detach _View" ~callback: (do_if_not_computing (fun () -> @@ -2874,14 +2906,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); b#insert ~iter:b#start_iter "\t\t"; with _ -> ()); b#insert - "\n\tCoqIDE: a Gtk2 interface for Coq\n\ - \nMain author : Benjamin Monate\ - \nContributors : Jean-Christophe Filliâtre\ - \n Pierre Letouzey, Claude Marché\n\ - \nFeature wish or bug report: use Web interface\n\ - \n\thttp://coq.inria.fr/bin/coq-bugs\n\ - \nVersion information\ - \n-------------------\n"; + "\nCoqIDE: an Integrated Development Environment for Coq\n\ + \nMain author : Benjamin Monate\ + \nContributors : Jean-Christophe Filliâtre\ + \n Pierre Letouzey, Claude Marché\n\ + \nFeature wish or bug report: use Web interface\n\ + \n\thttp://coq.inria.fr/bin/coq-bugs\n\ + \nVersion information\ + \n-------------------\n"; b#insert ((Coq.version ())) in @@ -2915,7 +2947,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); tv2#misc#modify_font !current.text_font; tv3#misc#modify_font !current.text_font; ignore (about_m#connect#activate - ~callback:(fun () -> about tv3#buffer)); + ~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer)); ignore (faq_m#connect#activate ~callback:(fun () -> load (Filename.concat lib_ide "FAQ"))); diff --git a/ide/preferences.ml b/ide/preferences.ml index 2bc92eeb5..64bb9c488 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -90,6 +90,8 @@ type pref = mutable contextual_menus_on_goal : bool; mutable window_width : int; mutable window_height :int; + mutable query_window_width : int; + mutable query_window_height : int; (* mutable use_utf8_notation : bool; *) @@ -100,7 +102,7 @@ let (current:pref ref) = ref { cmd_coqc = "coqc"; cmd_make = "make"; - cmd_coqmakefile = "coq_makefile -o Makefile *.v"; + cmd_coqmakefile = "coq_makefile -o makefile *.v"; cmd_coqdoc = "coqdoc -q -g"; cmd_print = "lpr"; @@ -115,12 +117,12 @@ let (current:pref ref) = encoding_use_utf8 = false; encoding_manual = "ISO_8859-1"; - automatic_tactics = ["Progress Trivial.","Trivial."; - "Tauto.","Tauto."; - "Progress Auto.","Auto."; - "Omega.","Omega."; - "Progress Auto with *.","Auto with *."; - "Progress Intuition.","Intuition."; + automatic_tactics = ["progress trivial.","trivial."; + "tauto.","tauto."; + "progress auto.","auto."; + "omega.","omega."; + "progress auto with *.","auto with *."; + "progress intuition.","intuition."; ]; modifier_for_navigation = [`CONTROL; `MOD1]; @@ -140,6 +142,8 @@ let (current:pref ref) = contextual_menus_on_goal = true; window_width = 800; window_height = 600; + query_window_width = 600; + query_window_height = 400; (* use_utf8_notation = false; *) @@ -202,6 +206,8 @@ let save_pref () = [string_of_bool p.contextual_menus_on_goal] ++ add "window_height" [string_of_int p.window_height] ++ add "window_width" [string_of_int p.window_width] ++ + add "query_window_height" [string_of_int p.query_window_height] ++ + add "query_window_width" [string_of_int p.query_window_width] ++ add "auto_complete" [string_of_bool p.auto_complete] ++ Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." @@ -257,6 +263,8 @@ let load_pref () = (fun v -> np.contextual_menus_on_goal <- v); set_int "window_width" (fun v -> np.window_width <- v); set_int "window_height" (fun v -> np.window_height <- v); + set_int "query_window_width" (fun v -> np.query_window_width <- v); + set_int "query_window_height" (fun v -> np.query_window_height <- v); set_bool "auto_complete" (fun v -> np.auto_complete <- v); current := np with e -> @@ -295,6 +303,7 @@ let configure () = !change_font !current.text_font) true in +(* let show_toolbar = bool ~f:(fun s -> @@ -317,6 +326,7 @@ let configure () = "Window width" (string_of_int !current.window_width) in +*) let auto_complete = bool ~f:(fun s -> @@ -333,8 +343,9 @@ let configure () = "Use Unicode Notation: " !current.use_utf8_notation in *) +(* let config_appearance = [show_toolbar; window_width; window_height] in - +*) let global_auto_revert = bool ~f:(fun s -> !current.global_auto_revert <- s) @@ -463,19 +474,20 @@ let configure () = let misc = [contextual_menus_on_goal;auto_complete] in let cmds = - [Section("Fonts", - [config_font]); - Section("Appearance", - config_appearance); - Section("Commands", - [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print]); - Section("Files", + [Section("Files", [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) encodings; ]); - Section("Browser", - [cmd_browse;doc_url;library_url]); + Section("Fonts", + [config_font]); +(* + Section("Appearance", + config_appearance); +*) + Section("Externals", + [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print; + cmd_browse;doc_url;library_url]); Section("Tactics Wizard", [automatic_tactics]); Section("Shortcuts", diff --git a/ide/preferences.mli b/ide/preferences.mli index 5cf26c90e..f6d163cb0 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -45,6 +45,8 @@ type pref = mutable contextual_menus_on_goal : bool; mutable window_width : int; mutable window_height : int; + mutable query_window_width : int; + mutable query_window_height : int; (* mutable use_utf8_notation : bool; *) -- cgit v1.2.3