diff options
author | 2011-04-01 09:42:35 +0000 | |
---|---|---|
committer | 2011-04-01 09:42:35 +0000 | |
commit | 0190a79581df3399b971264fb787af3294215fad (patch) | |
tree | 5f755c2305b850b447ec3a20ff74d998f7447386 /Source/ModelViewer/Main.cs | |
parent | dd270b5143e0f89abf8f5f80a747356b262b2f3a (diff) |
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
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 93 |
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
|