Add behavior to hide an empty taskbar in multi_desktop mode: tint2conf
This commit is contained in:
parent
d0e8450225
commit
0c36e79996
3 changed files with 19 additions and 0 deletions
|
@ -59,6 +59,7 @@ GtkWidget *taskbar_name_font, *taskbar_name_font_set;
|
|||
GtkWidget *taskbar_active_background, *taskbar_inactive_background;
|
||||
GtkWidget *taskbar_name_active_background, *taskbar_name_inactive_background;
|
||||
GtkWidget *taskbar_distribute_size, *taskbar_sort_order, *taskbar_alignment, *taskbar_always_show_all_desktop_tasks;
|
||||
GtkWidget *taskbar_hide_empty;
|
||||
|
||||
// task
|
||||
GtkWidget *task_mouse_left, *task_mouse_middle, *task_mouse_right, *task_mouse_scroll_up, *task_mouse_scroll_down;
|
||||
|
@ -3060,6 +3061,19 @@ void create_taskbar(GtkWidget *parent)
|
|||
col++;
|
||||
gtk_tooltips_set_tip(tooltips, taskbar_show_desktop, _("If enabled, the taskbar is split into multiple smaller taskbars, one for each virtual desktop."), NULL);
|
||||
|
||||
col = 2;
|
||||
row++;
|
||||
label = gtk_label_new(_("Hide taskbars for empty desktops"));
|
||||
gtk_misc_set_alignment(GTK_MISC(label), 0, 0);
|
||||
gtk_widget_show(label);
|
||||
gtk_table_attach(GTK_TABLE(table), label, col, col+1, row, row+1, GTK_FILL, 0, 0, 0);
|
||||
col++;
|
||||
|
||||
taskbar_hide_empty = gtk_check_button_new();
|
||||
gtk_widget_show(taskbar_hide_empty);
|
||||
gtk_table_attach(GTK_TABLE(table), taskbar_hide_empty, col, col+1, row, row+1, GTK_FILL, 0, 0, 0);
|
||||
col++;
|
||||
|
||||
col = 2;
|
||||
row++;
|
||||
label = gtk_label_new(_("Distribute size between taskbars"));
|
||||
|
|
|
@ -57,6 +57,7 @@ extern GtkWidget *taskbar_name_font, *taskbar_name_font_set;
|
|||
extern GtkWidget *taskbar_active_background, *taskbar_inactive_background;
|
||||
extern GtkWidget *taskbar_name_active_background, *taskbar_name_inactive_background;
|
||||
extern GtkWidget *taskbar_distribute_size, *taskbar_sort_order, *taskbar_alignment, *taskbar_always_show_all_desktop_tasks;
|
||||
extern GtkWidget *taskbar_hide_empty;
|
||||
|
||||
// task
|
||||
extern GtkWidget *task_mouse_left, *task_mouse_middle, *task_mouse_right, *task_mouse_scroll_up, *task_mouse_scroll_down;
|
||||
|
|
|
@ -295,6 +295,7 @@ void config_write_taskbar(FILE *fp)
|
|||
gtk_toggle_button_get_active(GTK_TOGGLE_BUTTON(taskbar_show_desktop)) ?
|
||||
"multi_desktop" :
|
||||
"single_desktop");
|
||||
fprintf(fp, "taskbar_hide_if_empty = %d\n", gtk_toggle_button_get_active(GTK_TOGGLE_BUTTON(taskbar_hide_empty)) ? 1 : 0);
|
||||
fprintf(fp,
|
||||
"taskbar_padding = %d %d %d\n",
|
||||
(int)gtk_spin_button_get_value(GTK_SPIN_BUTTON(taskbar_padding_x)),
|
||||
|
@ -1284,6 +1285,9 @@ void add_entry(char *key, char *value)
|
|||
else
|
||||
gtk_toggle_button_set_active(GTK_TOGGLE_BUTTON(taskbar_show_desktop), 0);
|
||||
}
|
||||
else if (strcmp(key, "taskbar_hide_if_empty") == 0) {
|
||||
gtk_toggle_button_set_active(GTK_TOGGLE_BUTTON(taskbar_hide_empty), atoi(value));
|
||||
}
|
||||
else if (strcmp(key, "taskbar_distribute_size") == 0) {
|
||||
gtk_toggle_button_set_active(GTK_TOGGLE_BUTTON(taskbar_distribute_size), atoi(value));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue