Introduce node categories; sort fields based on that not special characters

1 files changed, 16 insertions, 15 deletions

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 1330640e..57729e4d 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -11,6 +11,17 @@ namespace Microsoft.Boogie.ModelViewer
     public bool DebugMode;

   }

 

+  // sync with Main.categoryBrushes!

+  public enum NodeCategory

+  {

+    Local,

+    PhysField,

+    SpecField,

+    MethodologyProperty,

+    UserFunction,

+    Maplet

+  }

+

   public interface ILanguageProvider

   {

     bool IsMyModel(Model m);

@@ -27,7 +38,8 @@ namespace Microsoft.Boogie.ModelViewer
 

     IEnumerable<IState> States { get; }

 

-    IEnumerable<string> SortFields(IEnumerable<string> fields);

+    // This function is given IDisplayNode possibly from different states.

+    IEnumerable<string> SortFields(IEnumerable<IDisplayNode> fields);

   }

 

   public interface IState

@@ -36,13 +48,6 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<IDisplayNode> Nodes { get; }

   }

 

-  [Flags]

-  public enum NodeState

-  {

-    Normal = 0,

-    Changed = 1

-  }

-

   public interface IDisplayNode

   {

     /// <summary>

@@ -50,7 +55,7 @@ namespace Microsoft.Boogie.ModelViewer
     /// </summary>

     string Name { get; }

 

-    NodeState State { get; }

+    NodeCategory Category { get; }

     string Value { get; }

     string ToolTip { get; }

 

@@ -113,10 +118,8 @@ namespace Microsoft.Boogie.ModelViewer
       get { return null; }

     }

 

-    public virtual int ViewLevel

-    {

-      get; set;

-    }

+    public virtual int ViewLevel { get; set; }

+    public virtual NodeCategory Category { get; set; }

 

     public virtual IEnumerable<IDisplayNode> Children

     {

@@ -134,8 +137,6 @@ namespace Microsoft.Boogie.ModelViewer
     {

     }

 

-    public virtual NodeState State { get { return NodeState.Normal; } }

-

     public object ViewSync { get; set; }

 

     public virtual string Name