model viewer:

Allow opening model file via dialog
Added shortcut keys for the menu items
Made ReloadModel public so that we can use is as an entry point for a VS tool window

3 files changed, 116 insertions, 45 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index cb56bad5..e0e14058 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -51,6 +51,8 @@
       this.showSourceToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.menuStrip1 = new System.Windows.Forms.MenuStrip();

       this.fileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

+      this.openModelMenuItem = new System.Windows.Forms.ToolStripMenuItem();

+      this.toolStripSeparator1 = new System.Windows.Forms.ToolStripSeparator();

       this.reloadModelFileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.exitToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.viewToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

@@ -61,6 +63,7 @@
       this.toolStripMenuItem1 = new System.Windows.Forms.ToolStripSeparator();

       this.debugToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.modelsToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

+      this.openModelFileDialog = new System.Windows.Forms.OpenFileDialog();

       this.stateViewMenu.SuspendLayout();

       ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit();

       this.splitContainer1.Panel1.SuspendLayout();

@@ -171,9 +174,9 @@
       // 

       // matchesList

       // 

-      this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

-                  | System.Windows.Forms.AnchorStyles.Left)

-                  | System.Windows.Forms.AnchorStyles.Right)));

+      this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom) 

+            | System.Windows.Forms.AnchorStyles.Left) 

+            | System.Windows.Forms.AnchorStyles.Right)));

       this.matchesList.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {

             this.columnHeader4,

             this.columnHeader5});

@@ -229,9 +232,9 @@
       // 

       // textBox1

       // 

-      this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

-                  | System.Windows.Forms.AnchorStyles.Left)

-                  | System.Windows.Forms.AnchorStyles.Right)));

+      this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom) 

+            | System.Windows.Forms.AnchorStyles.Left) 

+            | System.Windows.Forms.AnchorStyles.Right)));

       this.textBox1.Location = new System.Drawing.Point(53, 3);

       this.textBox1.Name = "textBox1";

       this.textBox1.Size = new System.Drawing.Size(477, 20);

@@ -280,12 +283,12 @@
       this.contextMenuStrip1.Items.AddRange(new System.Windows.Forms.ToolStripItem[] {

             this.showSourceToolStripMenuItem});

       this.contextMenuStrip1.Name = "contextMenuStrip1";

-      this.contextMenuStrip1.Size = new System.Drawing.Size(153, 48);

+      this.contextMenuStrip1.Size = new System.Drawing.Size(142, 26);

       // 

       // showSourceToolStripMenuItem

       // 

       this.showSourceToolStripMenuItem.Name = "showSourceToolStripMenuItem";

-      this.showSourceToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.showSourceToolStripMenuItem.Size = new System.Drawing.Size(141, 22);

       this.showSourceToolStripMenuItem.Text = "Show source";

       this.showSourceToolStripMenuItem.Click += new System.EventHandler(this.showSourceToolStripMenuItem_Click);

       // 

@@ -304,23 +307,41 @@
       // fileToolStripMenuItem

       // 

       this.fileToolStripMenuItem.DropDownItems.AddRange(new System.Windows.Forms.ToolStripItem[] {

+            this.openModelMenuItem,

+            this.toolStripSeparator1,

             this.reloadModelFileToolStripMenuItem,

             this.exitToolStripMenuItem});

       this.fileToolStripMenuItem.Name = "fileToolStripMenuItem";

+      this.fileToolStripMenuItem.ShortcutKeys = ((System.Windows.Forms.Keys)((System.Windows.Forms.Keys.Alt | System.Windows.Forms.Keys.F4)));

       this.fileToolStripMenuItem.Size = new System.Drawing.Size(37, 20);

       this.fileToolStripMenuItem.Text = "&File";

       // 

+      // openModelMenuItem

+      // 

+      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.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);

+      // 

       // reloadModelFileToolStripMenuItem

       // 

       this.reloadModelFileToolStripMenuItem.Name = "reloadModelFileToolStripMenuItem";

-      this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(166, 22);

+      this.reloadModelFileToolStripMenuItem.ShortcutKeys = System.Windows.Forms.Keys.F5;

+      this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(213, 22);

       this.reloadModelFileToolStripMenuItem.Text = "&Reload model file";

       this.reloadModelFileToolStripMenuItem.Click += new System.EventHandler(this.reloadModelFileToolStripMenuItem_Click);

       // 

       // exitToolStripMenuItem

       // 

       this.exitToolStripMenuItem.Name = "exitToolStripMenuItem";

-      this.exitToolStripMenuItem.Size = new System.Drawing.Size(166, 22);

+      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.Text = "&Exit";

       this.exitToolStripMenuItem.Click += new System.EventHandler(this.exitToolStripMenuItem_Click);

       // 

@@ -342,40 +363,44 @@
       this.normalToolStripMenuItem.Checked = true;

       this.normalToolStripMenuItem.CheckState = System.Windows.Forms.CheckState.Checked;

       this.normalToolStripMenuItem.Name = "normalToolStripMenuItem";

-      this.normalToolStripMenuItem.Size = new System.Drawing.Size(199, 22);

+      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.Text = "&Normal";

       this.normalToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);

       // 

       // expertToolStripMenuItem

       // 

       this.expertToolStripMenuItem.Name = "expertToolStripMenuItem";

-      this.expertToolStripMenuItem.Size = new System.Drawing.Size(199, 22);

+      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.Text = "E&xpert";

       this.expertToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);

       // 

       // everythingToolStripMenuItem

       // 

       this.everythingToolStripMenuItem.Name = "everythingToolStripMenuItem";

-      this.everythingToolStripMenuItem.Size = new System.Drawing.Size(199, 22);

+      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.Text = "&Everything";

       this.everythingToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);

       // 

       // includeTheKitchenSinkToolStripMenuItem

       // 

       this.includeTheKitchenSinkToolStripMenuItem.Name = "includeTheKitchenSinkToolStripMenuItem";

-      this.includeTheKitchenSinkToolStripMenuItem.Size = new System.Drawing.Size(199, 22);

+      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.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(196, 6);

+      this.toolStripMenuItem1.Size = new System.Drawing.Size(239, 6);

       // 

       // debugToolStripMenuItem

       // 

       this.debugToolStripMenuItem.Name = "debugToolStripMenuItem";

-      this.debugToolStripMenuItem.Size = new System.Drawing.Size(199, 22);

+      this.debugToolStripMenuItem.Size = new System.Drawing.Size(242, 22);

       this.debugToolStripMenuItem.Text = "Debug";

       this.debugToolStripMenuItem.Click += new System.EventHandler(this.debugToolStripMenuItem_Click);

       // 

@@ -385,6 +410,11 @@
       this.modelsToolStripMenuItem.Size = new System.Drawing.Size(58, 20);

       this.modelsToolStripMenuItem.Text = "&Models";

       // 

+      // openModelFileDialog

+      // 

+      this.openModelFileDialog.Filter = "Model files (*.model)|*.model|All files (*.*)|*.*";

+      this.openModelFileDialog.Title = "Open model file";

+      // 

       // Main

       // 

       this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);

@@ -447,6 +477,9 @@
     private System.Windows.Forms.ToolStripMenuItem reloadModelFileToolStripMenuItem;

     private System.Windows.Forms.ContextMenuStrip contextMenuStrip1;

     private System.Windows.Forms.ToolStripMenuItem showSourceToolStripMenuItem;

+    private System.Windows.Forms.ToolStripMenuItem openModelMenuItem;

+    private System.Windows.Forms.ToolStripSeparator toolStripSeparator1;

+    private System.Windows.Forms.OpenFileDialog openModelFileDialog;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 13bb1b95..009a22a7 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -26,7 +26,7 @@ namespace Microsoft.Boogie.ModelViewer
     Model currentModel;

     Model[] allModels;

     int modelId;

-    string modelFileName;

+    string lastModelFileName;

     internal ViewOptions viewOpts = new ViewOptions();

 

     // TODO this should be dynamically loaded

@@ -63,45 +63,69 @@ namespace Microsoft.Boogie.ModelViewer
         System.Diagnostics.Debugger.Launch();

       }

 

-      if (filename == null)

-      {

-        throw new Exception("error: usage:  ModelViewer.exe MyProgram.model[:N]");  // (where does this exception go?)

-      }

-

+      if (filename != null)

       {

         var idx = filename.IndexOf(':');

-        if (idx > 0) {

+        if (idx > 0)

+        {

           modelId = int.Parse(filename.Substring(idx + 1));

           filename = filename.Substring(0, idx);

         }

       }

 

-      modelFileName = filename;

-      ReadModels();

-

-      this.Text = Path.GetFileName(filename) + " - Boogie Verification Debugger";

+      this.ReadModels(filename, this.modelId);

+    }

 

-      langProvider = null;

-      foreach (var p in Providers()) {

-        if (p.IsMyModel(currentModel)) {

-          langProvider = p;

-          break;

-        }

+    private void SetWindowTitle(string fileName)

+    {

+      if (fileName == null)

+      {

+        this.Text = "Boogie Verification Debugger";

+      }

+      else

+      {

+        this.Text = Path.GetFileName(fileName) + " - Boogie Verification Debugger";

       }

-

-      LoadModel(modelId);

     }

 

-    private void ReadModels()

+    public void ReadModels(string modelFileName, int setModelIdTo)

     {

-      using (var rd = File.OpenText(modelFileName)) {

-        allModels = Model.ParseModels(rd).ToArray();

+      this.lastModelFileName = modelFileName;

+      this.langProvider = Base.Provider.Instance;

+

+      if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName))

+      {

+        using (var rd = File.OpenText(modelFileName))

+        {

+          allModels = Model.ParseModels(rd).ToArray();

+        }

+

+        modelId = setModelIdTo;

+

+        if (modelId >= allModels.Length)

+          modelId = 0;

+

+        currentModel = allModels[modelId];

+        AddModelMenu();

+

+        foreach (var p in Providers())

+        {

+          if (p.IsMyModel(currentModel))

+          {

+            this.langProvider = p;

+            break;

+          }

+        }

+

+        LoadModel(modelId);

+      }

+      else

+      {

+        currentModel = new Model();

       }

-      if (modelId >= allModels.Length)

-        modelId = 0;

 

-      currentModel = allModels[modelId];

-      AddModelMenu();      

+      this.SetWindowTitle(modelFileName);

+

     }

 

     private void LoadModel(int idx)

@@ -130,7 +154,11 @@ namespace Microsoft.Boogie.ModelViewer
       var idx = 0;

       foreach (var m in allModels) {

         var currIdx = idx++; // this local needs to be in this block

-        modelsToolStripMenuItem.DropDownItems.Add(string.Format("Model #{0}", currIdx), null, (s, a) => LoadModel(currIdx));

+        var menuItem = modelsToolStripMenuItem.DropDownItems.Add(string.Format("Model #&{0}", currIdx), null, (s, a) => LoadModel(currIdx)) as ToolStripMenuItem;

+        if (currIdx <= 9)

+        {

+          menuItem.ShortcutKeys = Keys.Control | (Keys)(currIdx + Keys.D0);

+        }

       }

     }

 

@@ -619,8 +647,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void reloadModelFileToolStripMenuItem_Click(object sender, EventArgs e)

     {

-      ReadModels();

-      LoadModel(modelId);

+      ReadModels(this.lastModelFileName, this.modelId);

     }

 

     private SourceView sourceView;

@@ -648,6 +675,14 @@ namespace Microsoft.Boogie.ModelViewer
     {

       ShowSource();

     }

+

+    private void openModelMenuItem_Click(object sender, EventArgs e)

+    {

+      if (this.openModelFileDialog.ShowDialog() == System.Windows.Forms.DialogResult.OK)

+      {

+        this.ReadModels(this.openModelFileDialog.FileName, 0);

+      }

+    }

   }

 

   internal class DisplayItem : ListViewItem

diff --git a/Source/ModelViewer/Main.resx b/Source/ModelViewer/Main.resx
index 3d27240d..657b80c4 100644
--- a/Source/ModelViewer/Main.resx
+++ b/Source/ModelViewer/Main.resx
@@ -126,6 +126,9 @@
   <metadata name="menuStrip1.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

     <value>152, 17</value>

   </metadata>

+  <metadata name="openModelFileDialog.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

+    <value>422, 17</value>

+  </metadata>

   <assembly alias="System.Drawing" name="System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

   <data name="$this.Icon" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">

     <value>