diff options
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/DataModel.cs | 6 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.Designer.cs | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs index 4a1acb42..b6ec0bae 100644 --- a/Source/ModelViewer/DataModel.cs +++ b/Source/ModelViewer/DataModel.cs @@ -7,7 +7,11 @@ namespace Microsoft.Boogie.ModelViewer {
public class ViewOptions
{
- public int ViewLevel;
+ // 0 - Normal
+ // 1 - Expert
+ // 2 - Everything
+ // 3 - Include the kitchen sink
+ public int ViewLevel = 1;
public bool DebugMode;
}
diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs index 91d526d2..a58e7354 100644 --- a/Source/ModelViewer/Main.Designer.cs +++ b/Source/ModelViewer/Main.Designer.cs @@ -363,8 +363,6 @@ //
// normalToolStripMenuItem
//
- this.normalToolStripMenuItem.Checked = true;
- 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(240, 22);
@@ -373,6 +371,8 @@ //
// expertToolStripMenuItem
//
+ this.expertToolStripMenuItem.Checked = true;
+ this.expertToolStripMenuItem.CheckState = System.Windows.Forms.CheckState.Checked;
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(240, 22);
|