ui: added universal font size setting and shortcuts for changing it

This change adds font size and font family to the ApplicationSettings to have a single point for manipulating them. The
font size can also be changed via the menu or the zoomIn and zoomOut shortcuts on all platforms.
This commit is contained in:
Eberhard Graether
2015-07-15 00:38:10 +02:00
parent 7275082284
commit fb170cbd5d
46 changed files with 368 additions and 152 deletions
+1 -12
View File
@@ -13,7 +13,6 @@
border-top-left-radius: 10px;
border-top-right-radius: 10px;
margin-bottom: 5px;
min-height: 28px;
padding-right: 5px;
}
@@ -21,9 +20,8 @@
background: none;
border: none;
border-radius: 3px;
font-size: 14px;
padding: 2px 4px;
margin: 2px 8px;
margin: 1px 8px 3px;
}
#code_file #title_label:hover {
@@ -48,8 +46,6 @@
background: none;
color: gray;
border: none;
font-family: "Source Code Pro";
font-size: 14px;
}
#code_file #code_snippet #dots {
@@ -63,13 +59,6 @@
#code_area {
background-color: transparent;
font-family: "Source Code Pro";
font-size: 14px;
}
#code_area #line_number_area {
font-family: "Source Code Pro";
font-size: 14px;
}
#code_file #maximize_button, #code_file #snippet_button, #code_file #minimize_button {