summaryrefslogtreecommitdiff
path: root/Source/ModelViewer/TreeSkeleton.cs
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-10-14 21:46:08 +0000
committerGravatar MichalMoskal <unknown>2010-10-14 21:46:08 +0000
commit1f1182331f611acc691550e83f8ea2fd6890091c (patch)
tree1b62ce925b772e6d5cba3d4b0594ba08d3a6c19b /Source/ModelViewer/TreeSkeleton.cs
parenta827cc46921fcf06e248eaa6f32485779ee365f9 (diff)
Move SkeletonItem to a separate file
Diffstat (limited to 'Source/ModelViewer/TreeSkeleton.cs')
-rw-r--r--Source/ModelViewer/TreeSkeleton.cs98
1 files changed, 98 insertions, 0 deletions
diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
new file mode 100644
index 00000000..47f65e5d
--- /dev/null
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -0,0 +1,98 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Boogie.ModelViewer
+{
+ internal class SkeletonItem
+ {
+ readonly string name;
+ readonly List<SkeletonItem> children = new List<SkeletonItem>();
+ internal readonly IDisplayNode[] displayNodes;
+ readonly SkeletonItem parent;
+ readonly Main main;
+ internal readonly int level;
+ internal bool expanded, wasExpanded;
+
+ public void Iter(Action<SkeletonItem> handler)
+ {
+ handler(this);
+ children.Iter(u => u.Iter(handler));
+ }
+
+ public IEnumerable<SkeletonItem> RecChildren
+ {
+ get
+ {
+ if (expanded) {
+ foreach (var c in children) {
+ yield return c;
+ foreach (var ch in c.RecChildren)
+ yield return ch;
+ }
+ }
+ }
+ }
+
+ public void PopulateRoot(IEnumerable<IState> states)
+ {
+ var i = 0;
+ foreach (var s in states) {
+ displayNodes[i++] = new ContainerNode<IDisplayNode>(this.name, x => x, s.Nodes);
+ }
+ }
+
+ public SkeletonItem(Main m, int stateCount)
+ {
+ name = "<root>";
+ main = m;
+ displayNodes = new IDisplayNode[stateCount];
+ }
+
+ internal SkeletonItem(string n, SkeletonItem par)
+ : this(par.main, par.displayNodes.Length)
+ {
+ parent = par;
+ name = n;
+ level = par.level + 1;
+ }
+
+ public bool Expandable
+ {
+ get { return displayNodes.Any(d => d != null && d.Expandable); }
+ }
+
+ public bool Expanded
+ {
+ get { return expanded; }
+ set
+ {
+ if (!value) {
+ expanded = false;
+ } else {
+ if (expanded) return;
+ expanded = true;
+ if (wasExpanded) return;
+ wasExpanded = true;
+
+ var created = new Dictionary<string, SkeletonItem>();
+ for (int i = 0; i < displayNodes.Length; ++i) {
+ var dn = displayNodes[i];
+ if (dn == null || !dn.Expandable) continue;
+ foreach (var child in dn.Expand()) {
+ SkeletonItem skelChild;
+ if (!created.TryGetValue(child.EdgeName, out skelChild)) {
+ skelChild = new SkeletonItem(child.EdgeName, this);
+ created.Add(child.EdgeName, skelChild);
+ children.Add(skelChild);
+ }
+ skelChild.displayNodes[i] = child;
+ }
+ }
+ }
+ }
+ }
+ }
+
+}