update the menu bar (specifically, View > Show ...) after changes with "/"

This commit is contained in:
Werner Almesberger 2015-01-13 21:54:59 -03:00
parent 5fdea0e99a
commit e3deb3978f
3 changed files with 37 additions and 6 deletions

39
gui.c
View File

@ -11,6 +11,7 @@
*/
#include <stdlib.h>
#include <locale.h>
#include <gtk/gtk.h>
@ -132,26 +133,52 @@ static GtkItemFactoryEntry menu_entries[] = {
};
static GtkItemFactory *menu_factory;
static void make_menu_bar(GtkWidget *hbox)
{
GtkItemFactory *factory;
GtkWidget *bar;
factory = gtk_item_factory_new(GTK_TYPE_MENU_BAR, "<FpedMenu>", NULL);
gtk_item_factory_create_items(factory,
menu_factory = gtk_item_factory_new(GTK_TYPE_MENU_BAR, "<FpedMenu>",
NULL);
gtk_item_factory_create_items(menu_factory,
sizeof(menu_entries)/sizeof(*menu_entries), menu_entries, NULL);
bar = gtk_item_factory_get_widget(factory, "<FpedMenu>");
bar = gtk_item_factory_get_widget(menu_factory, "<FpedMenu>");
gtk_box_pack_start(GTK_BOX(hbox), bar, TRUE, TRUE, 0);
gtk_widget_set_sensitive(
gtk_item_factory_get_item(factory, "/File/Save"), !no_save);
gtk_item_factory_get_item(menu_factory, "/File/Save"), !no_save);
gtk_widget_set_sensitive(
gtk_item_factory_get_item(factory, "/File/Reload"),
gtk_item_factory_get_item(menu_factory, "/File/Reload"),
no_save && !!save_file_name);
}
void update_menu_bar(void)
{
const char *s;
switch (sidebar) {
case sidebar_var:
s = "/View/Show variables";
break;
case sidebar_code:
s = "/View/Show code";
break;
case sidebar_pkg:
s = "/View/Show packages";
break;
default:
abort();
}
gtk_check_menu_item_set_active(
GTK_CHECK_MENU_ITEM(gtk_item_factory_get_item(menu_factory, s)),
TRUE);
}
static gboolean toggle_all(GtkWidget *widget, GdkEventButton *event,
gpointer data)
{

3
gui.h
View File

@ -26,6 +26,9 @@ extern int show_bright;
extern int no_save;
/* update the menu bar after configuration changes */
void update_menu_bar(void);
/* update everything after a model change */
void change_world(void);

View File

@ -452,6 +452,7 @@ static gboolean key_press_event(GtkWidget *widget, GdkEventKey *event,
break;
case '/':
sidebar = sidebar == sidebar_last ? 0 : sidebar + 1;
update_menu_bar();
change_world();
break;
}