113
118
if(notebook.page_num (container) == -1) {
114
119
notebook.append_page (container, new Gtk.Label (_("Symbols")));
119
124
void remove_container () {
120
125
if (notebook.page_num (container) != -1)
121
126
notebook.remove (container);
134
130
if (refresh_timeout != 0)
135
131
Source.remove (refresh_timeout);