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

1 files changed, 64 insertions, 29 deletions

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