Add an ability to configure the font family for SQL editors. #392

pull/8587/head
Mike Christensen 2025-03-23 22:38:49 -07:00 committed by GitHub
parent fc1a1610a3
commit 13b44fffc7
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 18 additions and 1 deletions

Binary file not shown.

Before

Width:  |  Height:  |  Size: 193 KiB

After

Width:  |  Height:  |  Size: 96 KiB

View File

@ -417,6 +417,10 @@ Use the fields on the *Editor* panel to change settings of the query editor.
* When the *Code folding?* switch is set to *False*, the editor will disable
code folding. Disabling will improve editor performance with large files.
* Use the *Font family* field to specify the font family that will be used in
all SQL text boxes and editors. If the font is not found, the default font
of *Source Code Pro* will be used.
* Use the *Font size* field to specify the font size that will be used in text
boxes and editors.

View File

@ -301,8 +301,9 @@ export default function Editor({
const fontSize = calcFontSize(pref.sql_font_size);
newConfigExtn.push(EditorView.theme({
'.cm-content': {
'& .cm-content': {
fontSize: fontSize,
fontFamily: pref.sql_font_family,
},
'.cm-gutters': {
fontSize: fontSize,

View File

@ -390,6 +390,18 @@ def register_query_tool_preferences(self):
)
)
self.sql_font_family = self.preference.register(
'Editor', 'sql_font_family',
gettext("Font family"), 'text', 'Source Code Pro',
category_label=PREF_LABEL_DISPLAY,
help_str=gettext(
'Specify the font family to be used for all SQL editors. '
'The specified font should already be installed on your system. '
'If the font is not found, the editor will fall back to the '
'default font, Source Code Pro.'
)
)
self.display_connection_status = self.preference.register(
'display', 'connection_status',
gettext("Connection status"), 'boolean', True,