|
|
|
@ -34,31 +34,43 @@ class TabManager(GObject.Object): |
|
|
|
index = self.notebook.append_page(widget, header) |
|
|
|
index = self.notebook.append_page(widget, header) |
|
|
|
self.notebook.set_current_page(index) |
|
|
|
self.notebook.set_current_page(index) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def _read_source_file(self, source_file): |
|
|
|
|
|
|
|
if source_file is not None: |
|
|
|
|
|
|
|
with open(source_file, 'r') as f: |
|
|
|
|
|
|
|
return f.read() |
|
|
|
|
|
|
|
else: |
|
|
|
|
|
|
|
return None |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def new_tab(self, source_file): |
|
|
|
def new_tab(self, source_file): |
|
|
|
with open(source_file, 'r') as f: |
|
|
|
tab_id = self._next_tab_id() |
|
|
|
tab_id = self._next_tab_id() |
|
|
|
(sv, sv_controller) = self._init_sourceeditor() |
|
|
|
self.source_paths[tab_id] = source_file |
|
|
|
|
|
|
|
(sv, sv_controller) = self._init_sourceeditor() |
|
|
|
source = self._read_source_file(source_file) |
|
|
|
|
|
|
|
if source is not None: |
|
|
|
sv_controller.set_source_text(f.read()) |
|
|
|
sv_controller.set_source_text(f.read()) |
|
|
|
self.source_controllers[tab_id] = sv_controller |
|
|
|
|
|
|
|
self.widgets[tab_id] = sv |
|
|
|
self.source_paths[tab_id] = source_file |
|
|
|
sv.show_all() |
|
|
|
self.source_controllers[tab_id] = sv_controller |
|
|
|
header = Gtk.HBox() |
|
|
|
self.widgets[tab_id] = sv |
|
|
|
title_label = Gtk.Label(source_file) |
|
|
|
sv.show_all() |
|
|
|
image = Gtk.Image() |
|
|
|
header = Gtk.HBox() |
|
|
|
image.set_from_stock(Gtk.STOCK_CLOSE, Gtk.IconSize.MENU) |
|
|
|
title_label = Gtk.Label(source_file) |
|
|
|
close_button = Gtk.Button() |
|
|
|
image = Gtk.Image() |
|
|
|
close_button.set_image(image) |
|
|
|
image.set_from_stock(Gtk.STOCK_CLOSE, Gtk.IconSize.MENU) |
|
|
|
close_button.set_relief(Gtk.ReliefStyle.NONE) |
|
|
|
close_button = Gtk.Button() |
|
|
|
close_button.connect('clicked', self.close_cb, tab_id) |
|
|
|
close_button.set_image(image) |
|
|
|
|
|
|
|
close_button.set_relief(Gtk.ReliefStyle.NONE) |
|
|
|
header.pack_start(title_label, |
|
|
|
close_button.connect('clicked', self.close_cb, tab_id) |
|
|
|
expand=True, fill=True, padding=0) |
|
|
|
|
|
|
|
header.pack_end(close_button, |
|
|
|
header.pack_start(title_label, |
|
|
|
expand=False, fill=False, padding=0) |
|
|
|
expand=True, fill=True, padding=0) |
|
|
|
header.show_all() |
|
|
|
header.pack_end(close_button, |
|
|
|
index = self.notebook.append_page(sv, header) |
|
|
|
expand=False, fill=False, padding=0) |
|
|
|
self.notebook.set_current_page(index) |
|
|
|
header.show_all() |
|
|
|
|
|
|
|
index = self.notebook.append_page(sv, header) |
|
|
|
|
|
|
|
self.notebook.set_current_page(index) |
|
|
|
|
|
|
|
return tab_id |
|
|
|
|
|
|
|
|
|
|
|
def close_cb(self, arg, tab_id): |
|
|
|
def close_cb(self, arg, tab_id): |
|
|
|
index = self._widget_num_by_tab_id(tab_id) |
|
|
|
index = self._widget_num_by_tab_id(tab_id) |
|
|
|
@ -78,6 +90,10 @@ class TabManager(GObject.Object): |
|
|
|
|
|
|
|
|
|
|
|
return None |
|
|
|
return None |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def new_from_template(self, template): |
|
|
|
|
|
|
|
tab_id = self.new_tab(None) |
|
|
|
|
|
|
|
self.source_controllers[tab_id].set_source_text(template) |
|
|
|
|
|
|
|
|
|
|
|
def save_current(self): |
|
|
|
def save_current(self): |
|
|
|
index = self.notebook.get_current_page() |
|
|
|
index = self.notebook.get_current_page() |
|
|
|
w = self.notebook.get_nth_page(index) |
|
|
|
w = self.notebook.get_nth_page(index) |
|
|
|
|