Rename the Profile editor to a general preferences editor and only show a choice of profiles if there's more than one
This commit is contained in:
parent
6058727cdb
commit
26f0b2be69
|
@ -9,7 +9,7 @@ from keybindings import Keybindings
|
|||
from version import APP_NAME, APP_VERSION
|
||||
from translation import _
|
||||
|
||||
class ProfileEditor:
|
||||
class PrefsEditor:
|
||||
# lists of which settings to put in which tabs
|
||||
appearance = ['titlebars', 'zoomedtitlebar', 'allow_bold', 'audible_bell', 'visible_bell', 'urgent_bell', 'force_no_bell', 'background_darkness', 'background_type', 'background_image', 'cursor_blink', 'cursor_shape', 'font', 'scrollbar_position', 'scroll_background', 'use_system_font', 'use_theme_colors', 'enable_real_transparency']
|
||||
colours = ['foreground_color','background_color', 'cursor_color', 'palette', 'title_tx_txt_color', 'title_tx_bg_color', 'title_rx_txt_color', 'title_rx_bg_color', 'title_ia_txt_color', 'title_ia_bg_color']
|
|
@ -21,7 +21,6 @@ from newterminator import Terminator
|
|||
from titlebar import Titlebar
|
||||
from terminal_popup_menu import TerminalPopupMenu
|
||||
from searchbar import Searchbar
|
||||
from profileeditor import ProfileEditor
|
||||
from translation import _
|
||||
import plugin
|
||||
|
||||
|
|
|
@ -11,7 +11,7 @@ from translation import _
|
|||
from encoding import TerminatorEncoding
|
||||
from util import err
|
||||
from config import Config
|
||||
from profileeditor import ProfileEditor
|
||||
from prefseditor import PrefsEditor
|
||||
import plugin
|
||||
|
||||
class TerminalPopupMenu(object):
|
||||
|
@ -132,29 +132,30 @@ class TerminalPopupMenu(object):
|
|||
item.set_sensitive(False)
|
||||
menu.append(item)
|
||||
|
||||
item = gtk.MenuItem(_('_Preferences'))
|
||||
item.connect('activate', lambda x: PrefsEditor(self.terminal))
|
||||
menu.append(item)
|
||||
|
||||
config = Config()
|
||||
profilelist = config.list_profiles()
|
||||
|
||||
if len(profilelist) > 1:
|
||||
item = gtk.MenuItem(_('Profiles'))
|
||||
submenu = gtk.Menu()
|
||||
item.set_submenu(submenu)
|
||||
menu.append(item)
|
||||
|
||||
config = Config()
|
||||
current = terminal.get_profile()
|
||||
|
||||
group = None
|
||||
|
||||
for profile in config.list_profiles():
|
||||
for profile in profilelist():
|
||||
item = gtk.RadioMenuItem(group, profile.capitalize())
|
||||
item.connect('activate', terminal.set_profile, profile)
|
||||
if profile == current:
|
||||
item.set_active(True)
|
||||
submenu.append(item)
|
||||
|
||||
submenu.append(gtk.MenuItem())
|
||||
|
||||
item = gtk.MenuItem(_('Ed_it profiles'))
|
||||
item.connect('activate', lambda x: ProfileEditor(self.terminal))
|
||||
submenu.append(item)
|
||||
|
||||
self.add_encoding_items(menu)
|
||||
|
||||
try:
|
||||
|
|
Loading…
Reference in New Issue