+void
+on_optionsDiscardCore_activate (GtkMenuItem *menuitem,
+ gpointer user_data)
+{
+ end_text();
+ reset_focus();
+ ui.discard_corepointer =
+ gtk_check_menu_item_get_active(GTK_CHECK_MENU_ITEM (menuitem));
+ update_mappings_menu();
+}
+
+void
+on_fontButton_font_set (GtkFontButton *fontbutton,
+ gpointer user_data)
+{
+ gchar *str;
+
+ str = g_strdup(gtk_font_button_get_font_name(fontbutton));
+ process_font_sel(str);
+}
+
+void
+on_optionsLeftHanded_activate (GtkMenuItem *menuitem,
+ gpointer user_data)
+{
+ end_text();
+ reset_focus();
+ ui.left_handed = gtk_check_menu_item_get_active(GTK_CHECK_MENU_ITEM (menuitem));
+ gtk_scrolled_window_set_placement(GTK_SCROLLED_WINDOW(GET_COMPONENT("scrolledwindowMain")),
+ ui.left_handed?GTK_CORNER_TOP_RIGHT:GTK_CORNER_TOP_LEFT);
+}
+
+void
+on_optionsShortenMenus_activate (GtkMenuItem *menuitem,
+ gpointer user_data)
+{
+ gchar *item, *nextptr;
+ GtkWidget *w;
+
+ end_text();
+ reset_focus();
+ ui.shorten_menus = gtk_check_menu_item_get_active(GTK_CHECK_MENU_ITEM (menuitem));
+
+ /* go over the item list */
+ item = ui.shorten_menu_items;
+ while (*item==' ') item++;
+ while (*item) {
+ nextptr = strchr(item, ' ');
+ if (nextptr!=NULL) *nextptr = 0;
+ // hide or show the item
+ w = GET_COMPONENT(item);
+ if (w != NULL) {
+ if (ui.shorten_menus) gtk_widget_hide(w);
+ else gtk_widget_show(w);
+ }
+ // next item
+ if (nextptr==NULL) break;
+ *nextptr = ' ';
+ item = nextptr;
+ while (*item==' ') item++;
+ }
+
+ // just in case someone tried to unhide stuff they shouldn't be seeing
+ hide_unimplemented();
+ // maybe we should also make sure the drawing area stays visible ?
+}
+
+void
+on_optionsAutoSavePrefs_activate (GtkMenuItem *menuitem,
+ gpointer user_data)
+{
+ end_text();
+ reset_focus();
+ ui.auto_save_prefs = gtk_check_menu_item_get_active(GTK_CHECK_MENU_ITEM (menuitem));
+}
+
+void
+on_optionsPressureSensitive_activate (GtkMenuItem *menuitem,
+ gpointer user_data)
+{
+ int i;
+ end_text();
+ reset_focus();
+ ui.pressure_sensitivity =
+ gtk_check_menu_item_get_active(GTK_CHECK_MENU_ITEM (menuitem));
+ for (i=0; i<=NUM_BUTTONS; i++)
+ ui.brushes[i][TOOL_PEN].variable_width = ui.pressure_sensitivity;
+ update_mappings_menu();
+}
+