Add a diff preference for font size

This change adds a font size field in diff preferences in both the
generic preferences page and also the preferences modal from the diff
view. The new field allows users to update their preferred font size
for the diff view to be displayed. This updates both the line number
font size as well as the diff font size.

Feature: Issue 4417
Change-Id: I0fb75fd2186d2ff63b3627e8b0f15f2b3cddbfa3
This commit is contained in:
Becky Siegel
2016-10-12 10:55:26 -07:00
parent 9c4fae3bce
commit d7dbed640c
10 changed files with 51 additions and 4 deletions

View File

@@ -22,6 +22,9 @@ public class DiffPreferencesInfo {
/** Default tab size. */
public static final int DEFAULT_TAB_SIZE = 8;
/** Default font size. */
public static final int DEFAULT_FONT_SIZE = 12;
/** Default line length. */
public static final int DEFAULT_LINE_LENGTH = 100;
@@ -41,6 +44,7 @@ public class DiffPreferencesInfo {
public Integer context;
public Integer tabSize;
public Integer fontSize;
public Integer lineLength;
public Integer cursorBlinkRate;
public Boolean expandAllComments;
@@ -68,6 +72,7 @@ public class DiffPreferencesInfo {
DiffPreferencesInfo i = new DiffPreferencesInfo();
i.context = DEFAULT_CONTEXT;
i.tabSize = DEFAULT_TAB_SIZE;
i.fontSize = DEFAULT_FONT_SIZE;
i.lineLength = DEFAULT_LINE_LENGTH;
i.cursorBlinkRate = 0;
i.ignoreWhitespace = Whitespace.IGNORE_NONE;