1 files changed, 36 insertions, 51 deletions
diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index c4bae59e..8875cce6 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -15,22 +15,39 @@ namespace Microsoft.Boogie.ModelViewer.Base
       return true;
     }
 
-    IEnumerable<IDisplayNode> GetStateNodes(Model m)
+    public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
     {
-      yield return GenericNodes.Functions(m);
-      yield return GenericNodes.Constants(m);
-      foreach (var s in m.States)
-        yield return new StateNode(s);
+      return new GenericModel(m);
+    }
+  }
+
+  public class GenericModel : LanguageModel
+  {
+    Model m;
+
+    public GenericModel(Model m)
+    {
+      this.m = m;
     }
 
-    public IEnumerable<IState> GetStates(Model m)
+    public IDisplayNode Function(Model.Func f)
     {
-      yield return new TopState("TOP", GetStateNodes(m));
+      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);
     }
 
-    public IEnumerable<string> SortFields(IEnumerable<string> fields)
+    IEnumerable<IDisplayNode> GetStateNodes()
     {
-      return GlobalNamer.DefaultSortFields(fields);
+      yield return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);
+      yield return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.Functions);
+      foreach (var s in m.States)
+        yield return new StateNode(this, s);
+    }
+
+    public override IEnumerable<IState> States
+    {
+      get { 
+        yield return new TopState("TOP", GetStateNodes());
+      }
     }
   }
 
@@ -38,73 +55,41 @@ namespace Microsoft.Boogie.ModelViewer.Base
   {
     protected Model.CapturedState state;
 
-    public StateNode(Model.CapturedState s) : base(s.Name)
+    public StateNode(ILanguageSpecificModel p, Model.CapturedState s) : base(p, s.Name, null)
     {
       state = s;
     }
 
-    public override IEnumerable<string> Aliases
+    public override string Value
     {
-      get { foreach (var v in state.Variables) yield return v; }
+      get {
+        return state.Variables.Concat(", ");
+      }
     }
 
-    public override bool Expandable { get { return state.VariableCount != 0; } }
-
-    public override IEnumerable<IDisplayNode> Expand()
+    protected override void ComputeChildren()
     {
       foreach (var v in state.Variables) {
-        yield return new ElementNode(v, state.TryGet(v));
+        children.Add(new ElementNode(langModel, v, state.TryGet(v)));
       }
     }
   }
 
   public class ElementNode : DisplayNode
   {
-    protected Model.Element elt;
-
-    public ElementNode(string name, Model.Element elt) : base(name)
-    {
-      this.elt = elt;
-    }
-
-    public override IEnumerable<string> Aliases
-    {
-      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 ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}
   }
 
   public static class GenericNodes
   {
-    public static IDisplayNode Function(Model.Func f)
-    {
-      return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);
-    }
-
-    public static IDisplayNode Functions(Model m)
-    {
-      return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);
-    }
-
-    public static IDisplayNode Constants(Model m)
-    {
-      return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);
-    }
   }
 
   public class AppNode : ElementNode
   {
     protected Model.FuncTuple tupl;
 
-    public AppNode(Model.FuncTuple t)
-      : base(t.Func.Name, t.Result)
+    public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)
+      : base(m, t.Func.Name, t.Result)
     {
       tupl = t;
       var sb = new StringBuilder();