Add "Large font" menu item (for demos)

3 files changed, 61 insertions, 26 deletions

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<ILanguageProvider> 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);