diff options
| author |  wuestholz <unknown> | 2013-07-31 19:34:17 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-31 19:34:17 -0700 |
| commit | 0c1f7b1867df7c8f65a439125ab03d742f82988f (patch) | |
| tree | cd4cece45d0c1e7d2652e47b596d5854278ed511 /Source/ModelViewer | |
| parent | ab8d20ab0bda70a920c404538b74f1fea5dfb41c (diff) | |
Make it possible to set the font in BVD externally.
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/Main.cs | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index fde1971b..c15ea167 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -725,15 +725,19 @@ namespace Microsoft.Boogie.ModelViewer largeFont = new Font(smallFont.FontFamily, smallFont.Size * 2, smallFont.Unit);
}
- var font = largeFontToolStripMenuItem.Checked ? largeFont : smallFont;
- stateList.Font = font;
- currentStateView.Font = font;
- matchesList.Font = font;
+ SetFont(largeFontToolStripMenuItem.Checked ? largeFont : smallFont);
//textBox1.Font = font;
//linkLabel1.Font = font;
//label1.Font = font;
}
+ public void SetFont(System.Drawing.Font font)
+ {
+ stateList.Font = font;
+ currentStateView.Font = font;
+ matchesList.Font = font;
+ }
+
private void Main_Load(object sender, EventArgs e)
{
|