diff options
author | 2010-12-10 03:01:00 +0000 | |
---|---|---|
committer | 2010-12-10 03:01:00 +0000 | |
commit | 62fd1368ccccab299cf98d366286ac39cd82062d (patch) | |
tree | 50f02f59e245b3054eca86b49f4b93ba5e07ff6e /Source/ModelViewer/Main.cs | |
parent | fb350c313ff20b5a6de330e23d2c4577907070d7 (diff) |
Allow for model selection if there are multiple in the file
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 40 |
1 files changed, 36 insertions, 4 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 3466cd25..28744ac8 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -24,6 +24,7 @@ namespace Microsoft.Boogie.ModelViewer internal ILanguageSpecificModel langModel;
ToolStripMenuItem[] viewItems;
Model currentModel;
+ Model[] allModels;
internal ViewOptions viewOpts = new ViewOptions();
// TODO this should be dynamically loaded
@@ -46,25 +47,36 @@ namespace Microsoft.Boogie.ModelViewer var debugBreak = false;
string filename = null;
+
var args = Environment.GetCommandLineArgs();
for (int i = 1; i < args.Length; i++) {
var arg = args[i];
- if (arg == "/break")
+ if (arg == "/break" || arg == "-break")
debugBreak = true;
else
filename = arg;
}
+
if (debugBreak) {
System.Diagnostics.Debugger.Launch();
}
if (filename == null) {
- throw new Exception("error: usage: ModelViewer.exe MyProgram.model"); // (where does this exception go?)
+ throw new Exception("error: usage: ModelViewer.exe MyProgram.model[:N]"); // (where does this exception go?)
+ }
+
+ var modelId = 0;
+ {
+ var idx = filename.IndexOf(':');
+ if (idx > 0) {
+ modelId = int.Parse(filename.Substring(idx + 1));
+ filename = filename.Substring(0, idx);
+ }
}
using (var rd = File.OpenText(filename)) {
- var models = Model.ParseModels(rd);
- currentModel = models[0];
+ allModels = Model.ParseModels(rd).ToArray();
}
+ currentModel = allModels[modelId];
this.Text = Path.GetFileName(filename) + " - Boogie Verification Debugger";
@@ -76,9 +88,29 @@ namespace Microsoft.Boogie.ModelViewer }
}
+ AddModelMenu();
+ LoadModel(modelId);
+ }
+
+ private void LoadModel(int idx)
+ {
+ var i = 0;
+ foreach (ToolStripMenuItem it in modelsToolStripMenuItem.DropDownItems) {
+ it.Checked = i++ == idx;
+ }
+ currentModel = allModels[idx];
BuildModel();
}
+ private void AddModelMenu()
+ {
+ 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));
+ }
+ }
+
private void BuildModel()
{
stateList.Items.Clear();
|