diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index ba532bf6bb70d030348711525496e36ee9584603..4edc958567c6e270a7c08fdbf2aa0687b5ac1588 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -243,13 +243,7 @@ let insert (host_window: Design.main_window_extension_points) =
[ Menu_manager.menubar ~icon:stock "Exit Frama-C"
(Menu_manager.Unit_callback Cmdline.bail_out) ]
in
- quit_item.(0)#add_accelerator `CONTROL 'q';
- ignore
- (menu_manager#add_entries
- filemenu
- ~pos:0
- [ Menu_manager.toolbar ~icon:stock ~label:"Exit" ~tooltip:"Exit Frama-C"
- (Menu_manager.Unit_callback Cmdline.bail_out)])
+ quit_item.(0)#add_accelerator `CONTROL 'q'
(** Register this dialog in main window menu bar *)
let () = Design.register_extension insert
diff --git a/src/plugins/gui/menu_manager.mli b/src/plugins/gui/menu_manager.mli
index 5c0ae0244b3315c05721bf88e6decf4b03012b87..bac69d4bc08f09138084f0e99b712b1b5ef27f8e 100644
--- a/src/plugins/gui/menu_manager.mli
+++ b/src/plugins/gui/menu_manager.mli
@@ -54,8 +54,8 @@ type entry = private {
(** {2 Smart constructors for menu entries.}
- If not supplied, the [active] parameter is the function that always returns
- [true].
+ If not supplied, the [sensitive] parameter is the function that always
+ returns [true].
@since Nitrogen-20111001 *)
val toolbar:
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 23a8ecc27f0dd7f4ebc02e4697896bd6fde88c3d..2e60e840184f5cee1e0b02eb2744304e7b43ffe3 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -23,10 +23,11 @@
let compare_prj (_p1, n1) (_p2, n2) =
String.compare n1 n2
-let projects_list () =
+let projects_list ?(filter=fun _ -> true) () =
let projects =
Project.fold_on_projects
- (fun acc p -> (p, Project.get_unique_name p) :: acc)
+ (fun acc p ->
+ if filter p then ((p, Project.get_unique_name p) :: acc) else acc)
[]
in
List.sort compare_prj projects
@@ -37,8 +38,8 @@ let projects_list () =
module PrjRadiosSet =
FCSet.Make
(struct
- type t = (Project.t * string) * GMenu.radio_menu_item
- let compare (p1, _) (p2, _) = compare_prj p1 p2
+ type t = (Project.t * string) * GButton.radio_button * GMenu.menu_item
+ let compare (p1, _, _) (p2, _, _) = compare_prj p1 p2
end)
let project_radios : PrjRadiosSet.t ref = ref PrjRadiosSet.empty
@@ -138,32 +139,19 @@ let load_project (host_window: Design.main_window_extension_points) =
| `DELETE_EVENT | `CANCEL -> ());
dialog#destroy ()
-let rename_project (main_ui: Design.main_window_extension_points) project =
- let old = Project.get_unique_name project in
- let s =
- Gtk_helper.input_string
- ~parent:main_ui#main_window
- ~title:"Renaming project"
- (Format.sprintf "New name for project %S:" old)
- in
- match s with
- | None -> ()
- | Some s ->
- try
- ignore (Project.from_unique_name s);
- main_ui#error "Project of name %S already exists" s
- with Project.Unknown_project ->
- Project.set_name project s
+let mk_project_markup p =
+ let name = Project.get_unique_name p in
+ if Project.is_current p then "<b>" ^ name ^ "</b>" else name
-let reset (menu: GMenu.menu) =
+let reset ?filter (menu: GMenu.menu) =
(* Do not reset all if there is no change. *)
- let pl = projects_list () in
+ let pl = projects_list ?filter () in
let same_projects =
(* use that project_radios and pl are sorted in the same way *)
try
let rest =
PrjRadiosSet.fold
- (fun (p1, _) acc ->
+ (fun (p1, _, _) acc ->
match acc with
| [] -> raise Exit
| p2 :: acc ->
@@ -178,65 +166,91 @@ let reset (menu: GMenu.menu) =
if same_projects then begin
(* update the item status according to the current project anyway *)
PrjRadiosSet.iter
- (fun ((p, _), r) -> r#set_active (Project.is_current p))
+ (fun ((p, _), r, i) ->
+ r#set_active (Project.is_current p);
+ let widgets = i#children in
+ match widgets with
+ | [ w ] ->
+ (try
+ let label = GMisc.label_cast w in
+ label#set_label (mk_project_markup p);
+ label#set_use_markup true
+ with Gobject.Cannot_cast (t1,t2) ->
+ Gui_parameters.warning
+ "Child of project menu item of kind %s while %s was expected"
+ t1 t2)
+ | [] -> Gui_parameters.warning "Project menu item without child"
+ | _ -> Gui_parameters.warning "Project menu item with %d child"
+ (List.length widgets)
+ )
!project_radios;
false
end else begin
- PrjRadiosSet.iter
- (fun (_, r) -> menu#remove (r :> GMenu.menu_item))
- !project_radios;
+ PrjRadiosSet.iter (fun (_, _, i) -> menu#remove i) !project_radios;
project_radios := PrjRadiosSet.empty;
true
end
-let rec duplicate_project window menu project =
- let new_p =
- Project.create_by_copy ~last:false ~src:project (Project.get_name project)
+let duplicate_project project =
+ ignore
+ (Project.create_by_copy ~last:false ~src:project (Project.get_name project))
+
+let rec rename_project
+ (main_ui: Design.main_window_extension_points) menu project
+ =
+ let old = Project.get_unique_name project in
+ let s =
+ Gtk_helper.input_string
+ ~parent:main_ui#main_window
+ ~title:"Renaming project"
+ (Format.sprintf "New name for project %S:" old)
in
- try
- (* update the menu *)
- let group =
- let _, i = PrjRadiosSet.choose !project_radios in
- i#group
- in
- ignore (mk_project_entry window menu ~group new_p)
- with Not_found ->
- (* menu not built (action called from the toolbar) *)
- ()
+ (match s with
+ | None -> ()
+ | Some s ->
+ try
+ ignore (Project.from_unique_name s);
+ main_ui#error "Project of name %S already exists" s
+ with Project.Unknown_project ->
+ Project.set_name project s);
+ recompute main_ui menu
and mk_project_entry window menu ?group p =
- let p_item = GMenu.radio_menu_item
+ let pname = Project.get_unique_name p in
+ let markup = mk_project_markup p in
+ let item = GMenu.menu_item ~packing:menu#append () in
+ let _label = GMisc.label ~markup ~xalign:0. ~packing:item#add () in
+ let submenu = GMenu.menu ~packing:item#set_submenu () in
+ let current = GMenu.menu_item ~packing:submenu#append () in
+ let p_item = GButton.radio_button
?group
~active:(Project.is_current p)
- ~packing:menu#append
+ ~packing:current#add
+ ~label:"Set current"
()
in
- let callback () = if p_item#active then Project.set_current p in
- let pname = Project.get_unique_name p in
- ignore (p_item#connect#toggled ~callback);
- project_radios := PrjRadiosSet.add ((p, pname), p_item) !project_radios;
- let box = GPack.hbox ~packing:p_item#add () in
- ignore (GMisc.label ~text:pname ~packing:box#pack ());
- let buttons_box = GPack.hbox ~packing:(box#pack ~from:`END) () in
+ let callback () = Project.set_current p in
+ ignore (current#connect#activate ~callback);
+ project_radios := PrjRadiosSet.add ((p, pname), p_item, item) !project_radios;
let add_action stock text callback =
- let item = GButton.button ~packing:buttons_box#pack () in
- Gtk_helper.do_tooltip ~tooltip:text item;
- item#set_relief `NONE;
- let image = GMisc.image ~stock () in
- item#set_image image#coerce;
- image#set_icon_size `MENU;
- ignore (item#connect#clicked ~callback)
+ let image = GMisc.image ~xalign:0. ~stock () in
+ let image = image#coerce in
+ let item =
+ Gtk_helper.image_menu_item ~image ~text ~packing:submenu#append
+ in
+ ignore (item#connect#activate ~callback)
in
add_action `COPY "Duplicate project"
- (fun () -> duplicate_project window menu p);
+ (fun () -> duplicate_project p);
add_action `DELETE "Delete project" (fun () -> delete_project p);
add_action `SAVE "Save project" (fun () -> save_project window p);
add_action `SAVE_AS "Save project as" (fun () -> save_project_as window p);
- add_action `SELECT_FONT "Rename project" (fun () -> rename_project window p);
+ add_action
+ `SELECT_FONT "Rename project" (fun () -> rename_project window menu p);
p_item
-let make_project_entries window menu =
- match projects_list () with
+and make_project_entries ?filter window menu =
+ match projects_list ?filter () with
| [] -> assert false
| (pa, _name) :: tl ->
let mk = mk_project_entry window menu in
@@ -244,6 +258,10 @@ let make_project_entries window menu =
let group = pa_item#group in
List.iter (fun (pa, _) -> ignore (mk ~group pa)) tl
+and recompute ?filter window menu =
+ let is_reset = reset ?filter menu in
+ if is_reset then make_project_entries ?filter window menu
+
open Menu_manager
(** Register this dialog in main window menu bar *)
@@ -251,7 +269,7 @@ let () =
Design.register_extension
(fun window ->
let menu_manager = window#menu_manager () in
- let item, menu = menu_manager#add_menu "_Project" in
+ let _item, menu = menu_manager#add_menu "_Project" in
let constant_items =
menu_manager#add_entries
menu
@@ -262,23 +280,30 @@ let () =
(Unit_callback (fun () -> load_project window));
menubar ~icon:`COPY "Duplicate current project"
(Unit_callback
- (fun () -> duplicate_project window menu(Project.current())));
+ (fun () -> duplicate_project (Project.current())));
menubar ~icon:`DELETE "Delete current project"
(Unit_callback (fun () -> delete_project (Project.current ())));
menubar ~icon:`SELECT_FONT "Rename current project"
(Unit_callback
- (fun () -> rename_project window (Project.current ())));
+ (fun () -> rename_project window menu (Project.current ())));
]
in
let new_item = constant_items.(0) in
new_item#add_accelerator `CONTROL 'n';
constant_items.(3)#add_accelerator `CONTROL 'd';
ignore (GMenu.separator_item ~packing:menu#append ());
- let callback () =
- let is_reset = reset menu in
- if is_reset then make_project_entries window menu
+ let callback_prj _p = recompute window menu in
+ let callback_rm_prj p =
+ let filter p' = not (Project.equal p p') in
+ recompute ~filter window menu
in
- ignore (item#connect#activate ~callback))
+ let hook () = recompute window menu in
+ Project.register_create_hook callback_prj;
+ Project.register_after_set_current_hook ~user_only:true callback_prj;
+ Project.register_before_remove_hook callback_rm_prj;
+ Project.register_after_load_hook hook;
+ Project.register_after_global_load_hook hook;
+ recompute window menu)
(*
Local Variables: