From f165b7366f7751e8e85490a8ca94ac41c1aff279 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Fri, 15 Apr 2011 11:17:43 -0700 Subject: Add "Large font" menu item (for demos) --- Source/ModelViewer/Main.Designer.cs | 32 +++++++++++++++++---------- Source/ModelViewer/Main.cs | 44 +++++++++++++++++++++++++++---------- Source/ModelViewer/SourceView.cs | 11 +++++++--- 3 files changed, 61 insertions(+), 26 deletions(-) (limited to 'Source/ModelViewer') diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs index e0e14058..14a73a11 100644 --- a/Source/ModelViewer/Main.Designer.cs +++ b/Source/ModelViewer/Main.Designer.cs @@ -64,6 +64,7 @@ this.debugToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem(); this.modelsToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem(); this.openModelFileDialog = new System.Windows.Forms.OpenFileDialog(); + this.largeFontToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem(); this.stateViewMenu.SuspendLayout(); ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit(); this.splitContainer1.Panel1.SuspendLayout(); @@ -320,20 +321,20 @@ // this.openModelMenuItem.Name = "openModelMenuItem"; this.openModelMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Control | System.Windows.Forms.Keys.O))); - this.openModelMenuItem.Size = new System.Drawing.Size(213, 22); + this.openModelMenuItem.Size = new System.Drawing.Size(211, 22); this.openModelMenuItem.Text = "&Open model file..."; this.openModelMenuItem.Click += new System.EventHandler(this.openModelMenuItem_Click); // // toolStripSeparator1 // this.toolStripSeparator1.Name = "toolStripSeparator1"; - this.toolStripSeparator1.Size = new System.Drawing.Size(210, 6); + this.toolStripSeparator1.Size = new System.Drawing.Size(208, 6); // // reloadModelFileToolStripMenuItem // this.reloadModelFileToolStripMenuItem.Name = "reloadModelFileToolStripMenuItem"; this.reloadModelFileToolStripMenuItem.ShortcutKeys = System.Windows.Forms.Keys.F5; - this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(213, 22); + this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(211, 22); this.reloadModelFileToolStripMenuItem.Text = "&Reload model file"; this.reloadModelFileToolStripMenuItem.Click += new System.EventHandler(this.reloadModelFileToolStripMenuItem_Click); // @@ -341,7 +342,7 @@ // this.exitToolStripMenuItem.Name = "exitToolStripMenuItem"; this.exitToolStripMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Alt | System.Windows.Forms.Keys.F4))); - this.exitToolStripMenuItem.Size = new System.Drawing.Size(213, 22); + this.exitToolStripMenuItem.Size = new System.Drawing.Size(211, 22); this.exitToolStripMenuItem.Text = "&Exit"; this.exitToolStripMenuItem.Click += new System.EventHandler(this.exitToolStripMenuItem_Click); // @@ -353,7 +354,8 @@ this.everythingToolStripMenuItem, this.includeTheKitchenSinkToolStripMenuItem, this.toolStripMenuItem1, - this.debugToolStripMenuItem}); + this.debugToolStripMenuItem, + this.largeFontToolStripMenuItem}); this.viewToolStripMenuItem.Name = "viewToolStripMenuItem"; this.viewToolStripMenuItem.Size = new System.Drawing.Size(44, 20); this.viewToolStripMenuItem.Text = "&View"; @@ -364,7 +366,7 @@ this.normalToolStripMenuItem.CheckState = System.Windows.Forms.CheckState.Checked; this.normalToolStripMenuItem.Name = "normalToolStripMenuItem"; this.normalToolStripMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Control | System.Windows.Forms.Keys.N))); - this.normalToolStripMenuItem.Size = new System.Drawing.Size(242, 22); + this.normalToolStripMenuItem.Size = new System.Drawing.Size(240, 22); this.normalToolStripMenuItem.Text = "&Normal"; this.normalToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click); // @@ -372,7 +374,7 @@ // this.expertToolStripMenuItem.Name = "expertToolStripMenuItem"; this.expertToolStripMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Control | System.Windows.Forms.Keys.X))); - this.expertToolStripMenuItem.Size = new System.Drawing.Size(242, 22); + this.expertToolStripMenuItem.Size = new System.Drawing.Size(240, 22); this.expertToolStripMenuItem.Text = "E&xpert"; this.expertToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click); // @@ -380,7 +382,7 @@ // this.everythingToolStripMenuItem.Name = "everythingToolStripMenuItem"; this.everythingToolStripMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Control | System.Windows.Forms.Keys.E))); - this.everythingToolStripMenuItem.Size = new System.Drawing.Size(242, 22); + this.everythingToolStripMenuItem.Size = new System.Drawing.Size(240, 22); this.everythingToolStripMenuItem.Text = "&Everything"; this.everythingToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click); // @@ -388,19 +390,19 @@ // this.includeTheKitchenSinkToolStripMenuItem.Name = "includeTheKitchenSinkToolStripMenuItem"; this.includeTheKitchenSinkToolStripMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Control | System.Windows.Forms.Keys.K))); - this.includeTheKitchenSinkToolStripMenuItem.Size = new System.Drawing.Size(242, 22); + this.includeTheKitchenSinkToolStripMenuItem.Size = new System.Drawing.Size(240, 22); this.includeTheKitchenSinkToolStripMenuItem.Text = "&Include the kitchen sink"; this.includeTheKitchenSinkToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click); // // toolStripMenuItem1 // this.toolStripMenuItem1.Name = "toolStripMenuItem1"; - this.toolStripMenuItem1.Size = new System.Drawing.Size(239, 6); + this.toolStripMenuItem1.Size = new System.Drawing.Size(237, 6); // // debugToolStripMenuItem // this.debugToolStripMenuItem.Name = "debugToolStripMenuItem"; - this.debugToolStripMenuItem.Size = new System.Drawing.Size(242, 22); + this.debugToolStripMenuItem.Size = new System.Drawing.Size(240, 22); this.debugToolStripMenuItem.Text = "Debug"; this.debugToolStripMenuItem.Click += new System.EventHandler(this.debugToolStripMenuItem_Click); // @@ -415,6 +417,13 @@ this.openModelFileDialog.Filter = "Model files (*.model)|*.model|All files (*.*)|*.*"; this.openModelFileDialog.Title = "Open model file"; // + // largeFontToolStripMenuItem + // + this.largeFontToolStripMenuItem.Name = "largeFontToolStripMenuItem"; + this.largeFontToolStripMenuItem.Size = new System.Drawing.Size(240, 22); + this.largeFontToolStripMenuItem.Text = "Large font"; + this.largeFontToolStripMenuItem.Click += new System.EventHandler(this.largeFontToolStripMenuItem_Click); + // // Main // this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F); @@ -480,6 +489,7 @@ private System.Windows.Forms.ToolStripMenuItem openModelMenuItem; private System.Windows.Forms.ToolStripSeparator toolStripSeparator1; private System.Windows.Forms.OpenFileDialog openModelFileDialog; + private System.Windows.Forms.ToolStripMenuItem largeFontToolStripMenuItem; } diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 1c7286e7..fa03858b 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -27,6 +27,8 @@ namespace Microsoft.Boogie.ModelViewer int modelId; string lastModelFileName; internal ViewOptions viewOpts = new ViewOptions(); + Font smallFont, largeFont; + int lineHeight; // TODO this should be dynamically loaded IEnumerable Providers() @@ -40,6 +42,8 @@ namespace Microsoft.Boogie.ModelViewer { InitializeComponent(); + smallFont = stateList.Font; + if (runAsHostedWindow) { this.fileToolStripMenuItem.Enabled = false; @@ -239,9 +243,6 @@ namespace Microsoft.Boogie.ModelViewer } - const int levelMult = 16; - const int plusWidth = 16; - static Color Col(int c) { return Color.FromArgb(c >> 16, (c >> 8) & 0xff, c & 0xff); @@ -272,6 +273,7 @@ namespace Microsoft.Boogie.ModelViewer var skel = item.skel; var rect = e.Bounds; var listView = (ListView)sender; + lineHeight = rect.Height; rect.Y += 1; rect.Height -= 2; @@ -288,19 +290,19 @@ namespace Microsoft.Boogie.ModelViewer e.Graphics.FillRectangle(bg, rect); } - var off = levelMult * item.skel.level; + var off = lineHeight * item.skel.level; if (item.IsMatchListItem) off = 0; { var plusRect = rect; - plusRect.Width = plusWidth; + plusRect.Width = lineHeight; plusRect.X += off; var plusBorder = plusRect; - plusBorder.Height = 8; - plusBorder.Width = 8; - plusBorder.X += 4; - plusBorder.Y += 3; + plusBorder.Height = lineHeight / 2; + plusBorder.Width = lineHeight / 2; + plusBorder.X += lineHeight / 4; + plusBorder.Y += lineHeight / 4; e.Graphics.DrawRectangle(plusPen, plusBorder); if (skel.Expandable) { float midX = plusBorder.X + plusBorder.Width / 2; @@ -311,7 +313,7 @@ namespace Microsoft.Boogie.ModelViewer } } - off += plusWidth + 3; + off += lineHeight + 3; var nameRect = rect; var font = listView.Font; @@ -368,8 +370,8 @@ namespace Microsoft.Boogie.ModelViewer clickedItem.Focused = true; var skel = clickedItem.skel; - int plusLoc = skel.level * levelMult; - if (skel.Expandable && e.X >= plusLoc && e.X <= plusLoc + plusWidth) { + int plusLoc = skel.level * lineHeight; + if (skel.Expandable && e.X >= plusLoc && e.X <= plusLoc + lineHeight) { skel.Expanded = !skel.Expanded; SyncCurrentStateView(); } @@ -666,6 +668,7 @@ namespace Microsoft.Boogie.ModelViewer if (sourceView == null) { sourceView = new SourceView(); } + sourceView.largeFont = largeFontToolStripMenuItem.Checked; sourceView.SetSourceLocation(r); } } @@ -688,6 +691,23 @@ namespace Microsoft.Boogie.ModelViewer this.ReadModels(this.openModelFileDialog.FileName, 0); } } + + private void largeFontToolStripMenuItem_Click(object sender, EventArgs e) + { + largeFontToolStripMenuItem.Checked = !largeFontToolStripMenuItem.Checked; + + if (largeFont == null) { + 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; + //textBox1.Font = font; + //linkLabel1.Font = font; + //label1.Font = font; + } } internal class DisplayItem : ListViewItem diff --git a/Source/ModelViewer/SourceView.cs b/Source/ModelViewer/SourceView.cs index c8a8b653..d520ede5 100644 --- a/Source/ModelViewer/SourceView.cs +++ b/Source/ModelViewer/SourceView.cs @@ -11,9 +11,13 @@ namespace Microsoft.Boogie.ModelViewer { public partial class SourceView : Form { + public bool largeFont; + bool prevLarge; + public SourceView() { InitializeComponent(); + //richTextBox1.Font = new Font(richTextBox1.Font.FontFamily, fontSize, richTextBox1.Font.Unit); richTextBox1.BackColor = Color.White; } @@ -22,13 +26,14 @@ namespace Microsoft.Boogie.ModelViewer string prefix = @"{\rtf1\ansi\ansicpg1252\deff0\deflang1033{\fonttbl{\f0\fnil\fcharset0 Lucida Sans Typewriter;}}\r\n" + @"{\colortbl;\red0\green0\blue0;\red255\green0\blue0;\red0\green255\blue0;\red255\green255\blue0;\red0\green0\blue0;\red160\green160\blue160;}" + - @"\viewkind4\uc1\pard\f0\fs17 "; + @"\viewkind4\uc1\pard\f0"; internal void SetSourceLocation(SourceViewState r) { - if (r.RichTextContent != prevRtf) { - richTextBox1.Rtf = prefix + r.RichTextContent + "\r\n}\r\n"; + if (r.RichTextContent != prevRtf || prevLarge != largeFont) { + richTextBox1.Rtf = prefix + (largeFont ? "\\fs30 " : "\\fs17 ") + r.RichTextContent + "\r\n}\r\n"; prevRtf = r.RichTextContent; + prevLarge = largeFont; } richTextBox1.Select(r.Location, 9); -- cgit v1.2.3