Put in proper namespace, move files around.

9 files changed, 155 insertions, 154 deletions

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
new file mode 100644
index 00000000..f2250e0f
--- /dev/null
+++ b/Source/ModelViewer/DataModel.cs
@@ -0,0 +1,82 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie.ModelViewer

+{

+  public interface IDisplayNode

+  {

+    string Name { get; }

+    IEnumerable<string> Values { get; }

+    bool Expandable { get; }

+    IEnumerable<IDisplayNode> Expand();

+    object ViewSync { get; set; }

+  }

+

+  public class StateNode : IDisplayNode

+  {

+    protected Model.CapturedState state;

+

+    public StateNode(Model.CapturedState s)

+    {

+      state = s;

+    }

+

+    public virtual string Name

+    {

+      get { return "State"; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get { yield return state.Name; }

+    }

+

+    public virtual bool Expandable { get { return state.VariableCount != 0; } }

+

+    public virtual IEnumerable<IDisplayNode> Expand()

+    {

+      foreach (var v in state.Variables) {

+        yield return new ElementNode(v, state.TryGet(v));

+      }

+    }

+

+    public object ViewSync { get; set; }

+  }

+

+  public class ElementNode : IDisplayNode

+  {

+    protected Model.Element elt;

+    protected string name;

+

+    public ElementNode(string name, Model.Element elt)

+    {

+      this.name = name;

+      this.elt = elt;

+    }

+

+    public virtual string Name

+    {

+      get { return name; }

+    }

+

+    public virtual IEnumerable<string> Values

+    {

+      get

+      {

+        if (!(elt is Model.Uninterpreted))

+          yield return elt.ToString();

+        foreach (var tupl in elt.Names) {

+          if (tupl.Func.Arity == 0)

+            yield return tupl.Func.Name;

+        }

+      }

+    }

+

+    public virtual bool Expandable { get { return false; } }

+    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

+

+    public object ViewSync { get; set; }

+  }

+}

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 64aab748..f5a988b1 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -1,4 +1,4 @@
-namespace ModelViewer

+namespace Microsoft.Boogie.ModelViewer

 {

   partial class Main

   {

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 575721cd..8d06a9a0 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -11,7 +11,7 @@ using System.Windows.Forms;
 using System.IO;

 using Microsoft.Boogie;

 

-namespace ModelViewer

+namespace Microsoft.Boogie.ModelViewer

 {

   public partial class Main : Form

   {

@@ -71,6 +71,7 @@ namespace ModelViewer
       plusRect.Width = plusWidth;

       plusRect.X += off;

       e.Graphics.FillRectangle(Brushes.Gray, plusRect);

+      // TODO these should be icons

       e.Graphics.DrawString(item.expanded ? "[-]" : "[+]", listView1.Font, Brushes.Black, plusRect); // , StringFormat.GenericDefault);

 

       off += plusWidth + 3;

@@ -134,7 +135,7 @@ namespace ModelViewer
             var beg = clickedItem.Index + 1;

             for (int i = beg; i < listView1.Items.Count; ++i) {

               var curr = (DisplayItem)listView1.Items[i];

-              if (curr.level == clickedItem.level) break;

+              if (curr.level <= clickedItem.level) break;

               collapsed.Add(curr);

             }

             clickedItem.collapsedChildren = collapsed.ToArray();

@@ -181,77 +182,4 @@ namespace ModelViewer
       this.SubItems.Add(sb.ToString());

     }

   }

-

-  public interface IDisplayNode

-  {

-    string Name { get; }

-    IEnumerable<string> Values { get; }

-    bool Expandable { get; }

-    IEnumerable<IDisplayNode> Expand();

-    object ViewSync { get; set; }

-  }

-

-  public class StateNode : IDisplayNode

-  {

-    protected Model.CapturedState state;

-

-    public StateNode(Model.CapturedState s)

-    {

-      state = s;

-    }

-

-    public virtual string Name

-    {

-      get { return "State"; }

-    }

-

-    public virtual IEnumerable<string> Values

-    {

-      get { yield return state.Name; }

-    }

-

-    public virtual bool Expandable { get { return state.VariableCount != 0; } }

-    

-    public virtual IEnumerable<IDisplayNode> Expand()

-    {

-      foreach (var v in state.Variables) {

-        yield return new ElementNode(v, state.TryGet(v));

-      }

-    }

-

-    public object ViewSync { get; set; }

-  }

-

-  public class ElementNode : IDisplayNode

-  {

-    protected Model.Element elt;

-    protected string name;

-

-    public ElementNode(string name, Model.Element elt) { 

-      this.name = name; 

-      this.elt = elt; 

-    }

-

-    public virtual string Name

-    {

-      get { return name; }

-    }

-

-    public virtual IEnumerable<string> Values

-    {

-      get {

-        if (!(elt is Model.Uninterpreted))

-          yield return elt.ToString();

-        foreach (var tupl in elt.Names) {

-          if (tupl.Func.Arity == 0)

-            yield return tupl.Func.Name;

-        }

-      }

-    }

-

-    public virtual bool Expandable { get { return false; } }

-    public virtual IEnumerable<IDisplayNode> Expand() { yield break; }

-

-    public object ViewSync { get; set; }

-  }

 }

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index db4e039c..93270c46 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -8,7 +8,7 @@
     <ProjectGuid>{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}</ProjectGuid>

     <OutputType>WinExe</OutputType>

     <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>ModelViewer</RootNamespace>

+    <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>

     <AssemblyName>ModelViewer</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

@@ -46,6 +46,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

+    <Compile Include="DataModel.cs" />

     <Compile Include="Main.cs">

       <SubType>Form</SubType>

     </Compile>

@@ -72,6 +73,7 @@
     <Compile Include="Properties\Resources.Designer.cs">

       <AutoGen>True</AutoGen>

       <DependentUpon>Resources.resx</DependentUpon>

+      <DesignTime>True</DesignTime>

     </Compile>

     <None Include="Properties\Settings.settings">

       <Generator>SettingsSingleFileGenerator</Generator>

@@ -91,4 +93,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/ModelViewer/Program.cs b/Source/ModelViewer/Program.cs
index ca2c85cc..3444fe9a 100644
--- a/Source/ModelViewer/Program.cs
+++ b/Source/ModelViewer/Program.cs
@@ -3,7 +3,7 @@ using System.Collections.Generic;
 using System.Linq;

 using System.Windows.Forms;

 

-namespace ModelViewer

+namespace Microsoft.Boogie.ModelViewer

 {

   static class Program

   {

diff --git a/Source/ModelViewer/Properties/Resources.Designer.cs b/Source/ModelViewer/Properties/Resources.Designer.cs
index 3ed62cd5..2a56d355 100644
--- a/Source/ModelViewer/Properties/Resources.Designer.cs
+++ b/Source/ModelViewer/Properties/Resources.Designer.cs
@@ -8,63 +8,56 @@
 // </auto-generated>

 //------------------------------------------------------------------------------

 

-namespace ModelViewer.Properties

-{

-

-

-  /// <summary>

-  ///   A strongly-typed resource class, for looking up localized strings, etc.

-  /// </summary>

-  // This class was auto-generated by the StronglyTypedResourceBuilder

-  // class via a tool like ResGen or Visual Studio.

-  // To add or remove a member, edit your .ResX file then rerun ResGen

-  // with the /str option, or rebuild your VS project.

-  [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")]

-  [global::System.Diagnostics.DebuggerNonUserCodeAttribute()]

-  [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

-  internal class Resources

-  {

-

-    private static global::System.Resources.ResourceManager resourceMan;

-

-    private static global::System.Globalization.CultureInfo resourceCulture;

-

-    [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")]

-    internal Resources()

-    {

-    }

-

+namespace Microsoft.Boogie.ModelViewer.Properties {

+    using System;

+    

+    

     /// <summary>

-    ///   Returns the cached ResourceManager instance used by this class.

+    ///   A strongly-typed resource class, for looking up localized strings, etc.

     /// </summary>

-    [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

-    internal static global::System.Resources.ResourceManager ResourceManager

-    {

-      get

-      {

-        if ((resourceMan == null)) {

-          global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("ModelViewer.Properties.Resources", typeof(Resources).Assembly);

-          resourceMan = temp;

+    // This class was auto-generated by the StronglyTypedResourceBuilder

+    // class via a tool like ResGen or Visual Studio.

+    // To add or remove a member, edit your .ResX file then rerun ResGen

+    // with the /str option, or rebuild your VS project.

+    [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")]

+    [global::System.Diagnostics.DebuggerNonUserCodeAttribute()]

+    [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

+    internal class Resources {

+        

+        private static global::System.Resources.ResourceManager resourceMan;

+        

+        private static global::System.Globalization.CultureInfo resourceCulture;

+        

+        [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")]

+        internal Resources() {

+        }

+        

+        /// <summary>

+        ///   Returns the cached ResourceManager instance used by this class.

+        /// </summary>

+        [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

+        internal static global::System.Resources.ResourceManager ResourceManager {

+            get {

+                if (object.ReferenceEquals(resourceMan, null)) {

+                    global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("Microsoft.Boogie.ModelViewer.Properties.Resources", typeof(Resources).Assembly);

+                    resourceMan = temp;

+                }

+                return resourceMan;

+            }

+        }

+        

+        /// <summary>

+        ///   Overrides the current thread's CurrentUICulture property for all

+        ///   resource lookups using this strongly typed resource class.

+        /// </summary>

+        [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

+        internal static global::System.Globalization.CultureInfo Culture {

+            get {

+                return resourceCulture;

+            }

+            set {

+                resourceCulture = value;

+            }

         }

-        return resourceMan;

-      }

-    }

-

-    /// <summary>

-    ///   Overrides the current thread's CurrentUICulture property for all

-    ///   resource lookups using this strongly typed resource class.

-    /// </summary>

-    [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

-    internal static global::System.Globalization.CultureInfo Culture

-    {

-      get

-      {

-        return resourceCulture;

-      }

-      set

-      {

-        resourceCulture = value;

-      }

     }

-  }

 }

diff --git a/Source/ModelViewer/Properties/Settings.Designer.cs b/Source/ModelViewer/Properties/Settings.Designer.cs
index 5f03f3a1..d210a94e 100644
--- a/Source/ModelViewer/Properties/Settings.Designer.cs
+++ b/Source/ModelViewer/Properties/Settings.Designer.cs
@@ -8,23 +8,19 @@
 // </auto-generated>

 //------------------------------------------------------------------------------

 

-namespace ModelViewer.Properties

-{

-

-

-  [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

-  [global::System.CodeDom.Compiler.GeneratedCodeAttribute("Microsoft.VisualStudio.Editors.SettingsDesigner.SettingsSingleFileGenerator", "10.0.0.0")]

-  internal sealed partial class Settings : global::System.Configuration.ApplicationSettingsBase

-  {

-

-    private static Settings defaultInstance = ((Settings)(global::System.Configuration.ApplicationSettingsBase.Synchronized(new Settings())));

-

-    public static Settings Default

-    {

-      get

-      {

-        return defaultInstance;

-      }

+namespace Microsoft.Boogie.ModelViewer.Properties {

+    

+    

+    [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

+    [global::System.CodeDom.Compiler.GeneratedCodeAttribute("Microsoft.VisualStudio.Editors.SettingsDesigner.SettingsSingleFileGenerator", "10.0.0.0")]

+    internal sealed partial class Settings : global::System.Configuration.ApplicationSettingsBase {

+        

+        private static Settings defaultInstance = ((Settings)(global::System.Configuration.ApplicationSettingsBase.Synchronized(new Settings())));

+        

+        public static Settings Default {

+            get {

+                return defaultInstance;

+            }

+        }

     }

-  }

 }

diff --git a/Source/ModelViewer/SearchBox.Designer.cs b/Source/ModelViewer/SearchBox.Designer.cs
index 0bf884ce..cbb7c4a1 100644
--- a/Source/ModelViewer/SearchBox.Designer.cs
+++ b/Source/ModelViewer/SearchBox.Designer.cs
@@ -1,4 +1,4 @@
-namespace ModelViewer

+namespace Microsoft.Boogie.ModelViewer

 {

   partial class SearchBox

   {

diff --git a/Source/ModelViewer/SearchBox.cs b/Source/ModelViewer/SearchBox.cs
index abe428b2..0f337ba5 100644
--- a/Source/ModelViewer/SearchBox.cs
+++ b/Source/ModelViewer/SearchBox.cs
@@ -7,7 +7,7 @@ using System.Linq;
 using System.Text;

 using System.Windows.Forms;

 

-namespace ModelViewer

+namespace Microsoft.Boogie.ModelViewer

 {

   public partial class SearchBox : Form

   {