From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Source/ModelViewer/Main.cs | 1740 ++++++++++++++++++++++----------------------
 1 file changed, 870 insertions(+), 870 deletions(-)

(limited to 'Source/ModelViewer/Main.cs')

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 5fed89da..4697e454 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -1,870 +1,870 @@
-using System;
-using System.Collections.Generic;
-using System.ComponentModel;
-using System.Data;
-using System.Drawing;
-using System.Drawing.Drawing2D;
-using System.Linq;
-using System.Text;
-using System.Windows.Forms;
-
-using System.IO;
-using Microsoft.Boogie;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie.ModelViewer
-{
-  public partial class Main : Form
-  {
-    SkeletonItem unfoldingRoot;
-    SkeletonItem[] allItems;
-    public int CurrentState, PreviousState = -1;
-    IState[] states;
-    internal ILanguageProvider langProvider;
-    public ILanguageSpecificModel LangModel;
-    ToolStripMenuItem[] viewItems;
-    Model currentModel;
-    Model[] allModels;
-    int modelId;
-    string lastModelFileName;
-    internal ViewOptions viewOpts = new ViewOptions();
-    Font smallFont, largeFont;
-    int lineHeight;
-
-    // TODO this should be dynamically loaded
-    IEnumerable<ILanguageProvider> Providers()
-    {
-      yield return BCT.Provider.Instance;
-      yield return Vcc.Provider.Instance;
-      yield return Dafny.Provider.Instance;
-      yield return Base.Provider.Instance;
-    }
-
-    public Main(string[] args, bool runAsHostedWindow = false)
-    {
-      InitializeComponent();
-
-      smallFont = stateList.Font;
-
-      if (runAsHostedWindow) {
-        this.fileToolStripMenuItem.Enabled = false;
-        this.fileToolStripMenuItem.Visible = false;
-      }
-
-      viewItems = new ToolStripMenuItem[] {
-        normalToolStripMenuItem,
-        expertToolStripMenuItem,
-        everythingToolStripMenuItem,
-        includeTheKitchenSinkToolStripMenuItem
-      };
-
-      var debugBreak = false;
-      string filename = null;
-
-      for (int i = 1; i < args.Length; i++) {
-        var arg = args[i];
-        if (arg == "/break" || arg == "-break")
-          debugBreak = true;
-        else
-          filename = arg;
-      }
-
-      if (debugBreak) {
-        System.Diagnostics.Debugger.Launch();
-      }
-
-      if (filename != null) {
-        var idx = filename.IndexOf(':');
-        if (idx > 0) {
-          modelId = int.Parse(filename.Substring(idx + 1));
-          filename = filename.Substring(0, idx);
-        }
-      }
-
-      this.ReadModels(filename, this.modelId);
-    }
-
-    private void SetWindowTitle(string fileName)
-    {
-      if (fileName == null) {
-        this.Text = "Boogie Verification Debugger";
-      } else {
-        this.Text = Path.GetFileName(fileName) + " - Boogie Verification Debugger";
-      }
-    }
-
-    public void ReadModel(string model, int setModelIdTo = 0)
-    {
-      Contract.Requires(model != null);
-
-      using (var rd = new StringReader(model))
-      {
-        allModels = Model.ParseModels(rd).ToArray();
-      }
-
-      AddAndLoadModel(setModelIdTo);
-    }
-
-    public void ReadModels(string modelFileName, int setModelIdTo)
-    {
-      this.lastModelFileName = modelFileName;
-      this.langProvider = Base.Provider.Instance;
-
-      if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {
-        using (var rd = File.OpenText(modelFileName)) {
-          allModels = Model.ParseModels(rd).ToArray();
-        }
-
-        AddAndLoadModel(setModelIdTo);
-      } else {
-        currentModel = new Model();
-      }
-
-      this.SetWindowTitle(modelFileName);
-    }
-
-    private void AddAndLoadModel(int setModelIdTo)
-    {
-      modelId = setModelIdTo;
-
-      if (modelId >= allModels.Length)
-        modelId = 0;
-
-      currentModel = allModels[modelId];
-      AddModelMenu();
-
-      foreach (var p in Providers())
-      {
-        if (p.IsMyModel(currentModel))
-        {
-          this.langProvider = p;
-          break;
-        }
-      }
-
-      LoadModel(modelId);
-    }
-
-    private void LoadModel(int idx)
-    {
-      var i = 0;
-
-      //var stateIdx = stateList.SelectedIndices.Count == 0 ? 0 : stateList.SelectedIndices[0];
-
-      modelId = idx;
-      foreach (ToolStripMenuItem it in modelsToolStripMenuItem.DropDownItems) {
-        it.Checked = i++ == idx;
-      }
-      currentModel = allModels[idx];
-      BuildModel();
-
-      /*
-      if (stateList.Items.Count <= stateIdx)
-        stateIdx = 0;
-      stateList.Items[stateIdx].Selected = true;      
-       */
-    }
-
-    private void AddModelMenu()
-    {
-      modelsToolStripMenuItem.DropDownItems.Clear();
-      var idx = 0;
-      foreach (var m in allModels) {
-        var currIdx = idx++; // this local needs to be in this block
-        var menuItem = modelsToolStripMenuItem.DropDownItems.Add(string.Format("Model #&{0}", currIdx), null, (s, a) => LoadModel(currIdx)) as ToolStripMenuItem;
-        if (currIdx <= 9) {
-          menuItem.ShortcutKeys = Keys.Control | (Keys)(currIdx + Keys.D0);
-        }
-      }
-    }
-
-    private void BuildModel()
-    {
-      stateList.Items.Clear();
-
-      var items = new List<ListViewItem>();
-      LangModel = langProvider.GetLanguageSpecificModel(currentModel, viewOpts);
-      states = LangModel.States.ToArray();
-      var oldRoot = unfoldingRoot;
-      SkeletonItem selectedSkel = null;
-      if (oldRoot != null && SelectedNode() != null) {
-        selectedSkel = SelectedNode().skel;
-      }
-      unfoldingRoot = new SkeletonItem(this, states.Length);
-      allItems = unfoldingRoot.PopulateRoot(states);
-
-      var idx = 0;
-      foreach (var i in states) {
-        var it = new ListViewItem(new string[] { idx.ToString(), i.Name, "" });
-        it.Tag = i;
-        items.Add(it);
-        idx++;
-      }
-      stateList.Items.AddRange(items.ToArray());
-      unfoldingRoot.Expanded = true;
-
-      if (oldRoot == null) {
-        SetState(0);
-        stateList.Items[0].Selected = true;
-        SetColumnSizes();
-      } else {
-        var mapping = new Dictionary<SkeletonItem, SkeletonItem>();
-        unfoldingRoot.SyncWith(mapping, oldRoot);
-        SkeletonItem newIt = null;
-        while (selectedSkel != null) {
-          if (mapping.TryGetValue(selectedSkel, out newIt)) break;
-          selectedSkel = selectedSkel.parent;
-        }
-        if (CurrentState >= stateList.Items.Count)
-          CurrentState = 0;
-        if (PreviousState >= stateList.Items.Count)
-          PreviousState = -1;
-        if (newIt != null) GotoNode(newIt);
-        SyncStateListValues();
-        UpdateMatches(true);
-      }
-    }
-
-    private void SetColumnSizes()
-    {
-      currentStateView.Columns[0].Width = currentStateView.Width - currentStateView.Columns[1].Width - currentStateView.Columns[2].Width - 25;
-      stateList.Columns[1].Width = stateList.Width - stateList.Columns[0].Width - stateList.Columns[2].Width - 25;
-    }
-
-    public void SetState(int id, bool updateView = false)
-    {
-      if (updateView)
-      {
-        stateList.SelectedIndices.Clear();
-        stateList.SelectedIndices.Add(id);
-      }
-      if (CurrentState != id) {
-        PreviousState = CurrentState;
-        CurrentState = id;
-      }
-      UpdateMatches(true);
-    }
-
-    public void HideStateList()
-    {
-      stateList.Hide();
-      splitContainer1.Panel2.Hide();
-      splitContainer1.Panel2Collapsed = true;
-      splitContainer1.SplitterDistance = splitContainer1.Width;
-    }
-
-    public void HideMenuStrip()
-    {
-      menuStrip1.Hide();
-    }
-
-    internal void Activate(TreeNode treeNode)
-    {
-      throw new NotImplementedException();
-    }
-
-    private void listBox1_SelectedIndexChanged(object sender, EventArgs e)
-    {
-
-    }
-
-    static Color Col(int c)
-    {
-      return Color.FromArgb(c >> 16, (c >> 8) & 0xff, c & 0xff);
-    }
-
-    static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };
-    static Pen plusPen = new Pen(Col(0xaaaaaa));
-    static Brush grayedOut = new SolidBrush(Col(0xaaaaaa));
-    static Brush nonPrimary = new SolidBrush(Col(0xeeeeee));
-    static Brush matchBg = new SolidBrush(Col(0xFFFA6F));
-
-    static SolidBrush currentStateBrush = new SolidBrush(Color.Red);
-    static SolidBrush regularStateBrush = new SolidBrush(Color.Black);
-    static SolidBrush previousStateBrush = new SolidBrush(Color.Blue);
-
-    static SolidBrush[] categoryBrushes = new SolidBrush[] {
-      new SolidBrush(Color.Black), // Local
-      new SolidBrush(Color.Black), // PhysField
-      new SolidBrush(Color.Green), // SpecField
-      new SolidBrush(Color.Peru), // MethodologyProperty
-      new SolidBrush(Color.Green), // UserFunction
-      new SolidBrush(Color.Black), // Maplet
-    };
-
-    private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)
-    {
-      var item = (DisplayItem)e.Item;
-      var skel = item.skel;
-      var rect = e.Bounds;
-      var listView = (ListView)sender;
-      lineHeight = rect.Height;
-      rect.Y += 1;
-      rect.Height -= 2;
-
-      var textBrush = Brushes.Black;
-      if (listView.SelectedIndices.Count > 0 && listView.SelectedIndices[0] == e.ItemIndex) {
-        e.Graphics.FillRectangle(Brushes.Aquamarine, rect);
-        textBrush = Brushes.White;
-      } else {
-        var bg = Brushes.White;
-        if (item.active && !skel.isPrimary[CurrentState])
-          bg = nonPrimary;
-        if (item.skel.isMatch)
-          bg = matchBg;
-        e.Graphics.FillRectangle(bg, rect);
-      }
-
-      var off = lineHeight * item.skel.level;
-      if (item.IsMatchListItem)
-        off = 0;
-
-      {
-        var plusRect = rect;
-        plusRect.Width = lineHeight;
-        plusRect.X += off;
-        var plusBorder = plusRect;
-        plusBorder.Height = lineHeight / 2;
-        plusBorder.Width = lineHeight / 2;
-        plusBorder.X += lineHeight / 4;
-        plusBorder.Y += lineHeight / 4;
-        e.Graphics.DrawRectangle(plusPen, plusBorder);
-        if (skel.Expandable) {
-          float midX = plusBorder.X + plusBorder.Width / 2;
-          float midY = plusBorder.Y + plusBorder.Height / 2;
-          e.Graphics.DrawLine(plusPen, plusBorder.X + 2, midY, plusBorder.Right - 2, midY);
-          if (!item.skel.expanded)
-            e.Graphics.DrawLine(plusPen, midX, plusBorder.Y + 2, midX, plusBorder.Bottom - 2);
-        }
-      }
-
-      off += lineHeight + 3;
-      var nameRect = rect;
-      var font = listView.Font;
-
-      textBrush = categoryBrushes[(int)item.dispNode.Category];
-
-      if (!item.active)
-        textBrush = grayedOut;
-
-      nameRect.Width = listView.Columns[0].Width - 1 - off;
-      nameRect.X += off;
-      var width = DrawString(e.Graphics, item.SubItems[0].Text, font, textBrush, nameRect);
-
-      textBrush = item.active ? Brushes.Black : grayedOut;
-      nameRect.X += width + 4;
-      nameRect.Width = listView.Columns[0].Width + listView.Columns[1].Width - nameRect.X;
-      width = DrawString(e.Graphics, item.SubItems[1].Text, font, textBrush, nameRect);
-
-      nameRect.X += width + 4;
-      nameRect.Width = listView.Width - nameRect.X;
-      var t = item.SubItems[2].Text;
-      width = DrawString(e.Graphics, t, font, t == item.SubItems[1].Text ? grayedOut : Brushes.Black, nameRect);
-    }
-
-    private int DrawString(Graphics g, string s, Font font, Brush textBrush, Rectangle minRect)
-    {
-      var sz = g.MeasureString(s, font).Width;
-      if (sz > minRect.Width - 2) {
-        minRect.Width = (int)(sz + 20);
-      }
-      g.DrawString(s, font, textBrush, minRect);
-      return minRect.Width;
-    }
-
-    private void listView1_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e)
-    {
-      e.DrawBackground();
-      var brush = regularStateBrush;
-      if (e.Header.Index == 1)
-        brush = currentStateBrush;
-      else if (e.Header.Index == 2)
-        brush = previousStateBrush;
-
-      Rectangle r = e.Bounds;
-      r.X += 5;
-      r.Y += 4;
-      DrawString(e.Graphics, e.Header.Text, e.Header.ListView.Font, brush, r);
-    }
-
-    private void listView1_MouseUp(object sender, MouseEventArgs e)
-    {
-      var clickedItem = (DisplayItem)currentStateView.GetItemAt(5, e.Y);
-      if (clickedItem != null) {
-        clickedItem.Selected = true;
-        clickedItem.Focused = true;
-
-        var skel = clickedItem.skel;
-        int plusLoc = skel.level * lineHeight;
-        if (skel.Expandable && e.X >= plusLoc && e.X <= plusLoc + lineHeight) {
-          skel.Expanded = !skel.Expanded;
-          SyncCurrentStateView();
-        }
-      }
-    }
-
-    private void SyncCurrentStateView()
-    {
-      SyncListView(unfoldingRoot.RecChildren, currentStateView, (x, y) => { });
-    }
-
-    private void SyncListView(IEnumerable<SkeletonItem> items, ListView listView, Action<DisplayItem, SkeletonItem> cb)
-    {
-      var ch = items.ToArray();
-      var missing = ch.Length - listView.Items.Count;
-      listView.BeginUpdate();
-      if (missing < 0) {
-        missing = -missing;
-        while (missing-- > 0) {
-          listView.Items.RemoveAt(listView.Items.Count - 1);
-        }
-      } else {
-        while (missing-- > 0) {
-          listView.Items.Add(new DisplayItem());
-        }
-      }
-      for (int i = 0; i < ch.Length; ++i) {
-        var di = (DisplayItem)listView.Items[i];
-        cb(di, ch[i]);
-        di.Set(ch[i], CurrentState, PreviousState);
-      }
-      listView.EndUpdate();
-      listView.Invalidate();
-    }
-
-    private void listView1_ColumnWidthChanged(object sender, ColumnWidthChangedEventArgs e)
-    {
-      currentStateView.Invalidate();
-    }
-
-    private void listView1_Resize(object sender, EventArgs e)
-    {
-      SetColumnSizes();
-      currentStateView.Invalidate();
-    }
-
-    private void stateList_SelectedIndexChanged(object sender, EventArgs e)
-    {
-      if (stateList.SelectedItems.Count == 0) return;
-      var sel = stateList.SelectedItems[0].Index;
-
-      if (PreviousState >= 0)
-        stateList.Items[PreviousState].ForeColor = regularStateBrush.Color;
-
-      SetState(sel);
-    }
-
-    DisplayItem SelectedNode()
-    {
-      if (currentStateView.SelectedItems.Count == 0) return null;
-      return (DisplayItem)currentStateView.SelectedItems[0];
-    }
-
-    private void currentStateView_SelectedIndexChanged(object sender, EventArgs e)
-    {
-      SyncStateListValues();
-    }
-
-    private void SyncStateListValues()
-    {
-      var sel = SelectedNode();
-      if (sel == null) return;
-
-      stateList.BeginUpdate();
-      for (int i = 0; i < sel.skel.displayNodes.Length; ++i) {
-        var dn = sel.skel.displayNodes[i];
-        stateList.Items[i].SubItems[2].Text = dn == null ? "" : dn.Value;
-      }
-      stateList.EndUpdate();
-    }
-
-    private void ExpandParents(SkeletonItem item)
-    {
-      item = item.parent;
-      while (item != null) {
-        item.Expanded = true;
-        item = item.parent;
-      }
-    }
-
-    private void textBox1_TextChanged(object sender, EventArgs e)
-    {
-      UpdateMatches(false);
-    }
-
-    private void UpdateMatches(bool force)
-    {
-      var bad = false;
-      Model.Element eltEq = null;
-      var eltRef = new List<Model.Element>();
-      var words = new List<string>();
-
-      foreach (var w in textBox1.Text.Split(' ')) {
-        if (w == "") continue;
-        if (w.StartsWith("eq:")) {
-          if (eltEq != null) bad = true;
-          else {
-            eltEq = LangModel.FindElement(w.Substring(3));
-            if (eltEq == null) bad = true;
-          }
-        } else if (w.StartsWith("use:")) {
-          var e = LangModel.FindElement(w.Substring(4));
-          if (e == null) bad = true;
-          else eltRef.Add(e);
-        } else {
-          words.Add(w.ToLower());
-        }
-      }
-
-      textBox1.ForeColor = bad ? Color.Red : Color.Black;
-
-      var wordsA = words.ToArray();
-      var refsA = eltRef.ToArray();
-
-      if (eltEq == null && wordsA.Length == 0 && refsA.Length == 0)
-        bad = true;
-
-      var changed = true; // force;
-      var matches = new List<SkeletonItem>();
-
-      foreach (var s in allItems) {
-        var newMatch = false;
-        if (s.isPrimary[CurrentState] && !bad) {
-          newMatch = s.MatchesWords(wordsA, refsA, eltEq, CurrentState);
-        }
-        if (newMatch)
-          matches.Add(s);
-        if (s.isMatch != newMatch) {
-          changed = true;
-          s.isMatch = newMatch;
-        }
-      }
-
-      if (PreviousState >= 0)
-        stateList.Items[PreviousState].ForeColor = previousStateBrush.Color;
-      stateList.Items[CurrentState].ForeColor = currentStateBrush.Color;
-
-      if (changed) {
-        SyncListView(matches, matchesList, (di, _) => { di.IsMatchListItem = true; });
-        SyncCurrentStateView();
-      }
-    }
-
-    private void matchesList_Resize(object sender, EventArgs e)
-    {
-      matchesList.Invalidate();
-    }
-
-    private void matchesList_DoubleClick(object sender, EventArgs e)
-    {
-      if (matchesList.SelectedItems.Count == 0) return;
-      var sel = (DisplayItem)matchesList.SelectedItems[0];
-      GotoNode(sel.skel);
-    }
-
-    private void linkLabel1_LinkClicked(object sender, LinkLabelLinkClickedEventArgs e)
-    {
-      foreach (DisplayItem it in matchesList.Items) {
-        ExpandParents(it.skel);
-      }
-      SyncCurrentStateView();
-    }
-
-    private void SetSearch(string text)
-    {
-      textBox1.Text = text;
-    }
-
-    private void GotoNode(SkeletonItem skel)
-    {
-      ExpandParents(skel);
-      SyncCurrentStateView();
-      foreach (DisplayItem it in currentStateView.Items) {
-        if (it.skel == skel) {
-          it.Selected = true;
-          currentStateView.EnsureVisible(it.Index);
-          break;
-        }
-      }
-    }
-
-    private IEnumerable<SkeletonItem> NamesFor(Model.Element elt)
-    {
-      var words = new string[0];
-      var elts = new Model.Element[0];
-
-      foreach (var s in allItems) {
-        if (s.isPrimary[CurrentState] && s.MatchesWords(words, elts, elt, CurrentState)) {
-          yield return s;
-        }
-      }
-    }
-
-    private void AddMenuItems(IEnumerable<SkeletonItem> skels, ToolStripItemCollection items, string pref, int max)
-    {
-      var skelsM = skels.Take(max).ToArray();
-
-      foreach (var s in skelsM) {
-        var tmp = s;
-        items.Add(pref + s.LongName(CurrentState), null, (x, _) => GotoNode(tmp));
-      }
-
-      if (skelsM.Length == max)
-        items.Add(new ToolStripMenuItem("...") { Enabled = false });
-    }
-
-    private void stateViewMenu_Opening(object sender, CancelEventArgs e)
-    {
-      IDisplayNode sel = null;
-      SkeletonItem skel = null;
-      if (SelectedNode() != null) {
-        sel = SelectedNode().dispNode;
-        skel = SelectedNode().skel;
-      }
-
-      var items = stateViewMenu.Items;
-      items.Clear();
-
-      if (sel == null) {
-        items.Add(new ToolStripMenuItem("Unavailable") { Enabled = false });
-        return;
-      }
-
-      foreach (var x in sel.References.Where(q => q != sel.Element)) {
-        var t = new ToolStripMenuItem(LangModel.CanonicalName(x));
-        items.Add(t);
-        AddMenuItems(NamesFor(x), t.DropDownItems, "= ", 20);
-      }
-
-      if (sel.Element != null) {
-        var selName = LangModel.CanonicalName(sel.Element);
-        items.Add("Find uses...", null, (s, _) => SetSearch("use:" + selName));
-
-        var aliases = NamesFor(sel.Element).Where(s => s != skel).ToArray();
-        if (aliases.Length > 0) {
-          items.Add("Aliases...", null, (s, _) => SetSearch("eq:" + selName));
-          AddMenuItems(aliases, items, "   = ", 10);
-        }
-      }
-    }
-
-    private void normalToolStripMenuItem_Click(object sender, EventArgs e)
-    {
-      int viewLev = -1;
-      for (int i = 0; i < viewItems.Length; ++i) {
-        if (viewItems[i] == sender) {
-          viewLev = i;
-          viewItems[i].Checked = true;
-        } else {
-          viewItems[i].Checked = false;
-        }
-      }
-      if (viewLev != -1 && viewLev != viewOpts.ViewLevel) {
-        viewOpts.ViewLevel = viewLev;
-        BuildModel();
-      }
-    }
-
-    private void debugToolStripMenuItem_Click(object sender, EventArgs e)
-    {
-      debugToolStripMenuItem.Checked = !debugToolStripMenuItem.Checked;
-      viewOpts.DebugMode = debugToolStripMenuItem.Checked;
-      BuildModel();
-    }
-
-    private void exitToolStripMenuItem_Click(object sender, EventArgs e)
-    {
-      this.Close();
-    }
-
-    private void reloadModelFileToolStripMenuItem_Click(object sender, EventArgs e)
-    {
-      ReadModels(this.lastModelFileName, this.modelId);
-    }
-
-    private SourceView sourceView;
-    private void ShowSource()
-    {
-      if (stateList.SelectedItems.Count == 0) return;
-      var li = stateList.SelectedItems[0] as ListViewItem;
-      if (li != null) {
-        var r = ((IState)li.Tag).ShowSource();
-        if (r != null) {
-          if (sourceView == null) {
-            sourceView = new SourceView();
-          }
-          sourceView.largeFont = largeFontToolStripMenuItem.Checked;
-          sourceView.SetSourceLocation(r);
-          sourceView.BringToFront();
-        }
-      }
-    }
-
-    private void showSourceToolStripMenuItem_Click(object sender, EventArgs e)
-    {
-      ShowSource();
-    }
-
-    private void stateList_DoubleClick(object sender, EventArgs e)
-    {
-      ShowSource();
-    }
-
-    private void openModelMenuItem_Click(object sender, EventArgs e)
-    {
-      if (this.openModelFileDialog.ShowDialog() == System.Windows.Forms.DialogResult.OK) {
-        this.ReadModels(this.openModelFileDialog.FileName, 0);
-      }
-    }
-
-    private void largeFontToolStripMenuItem_Click(object sender, EventArgs e)
-    {
-      largeFontToolStripMenuItem.Checked = !largeFontToolStripMenuItem.Checked;
-
-      if (largeFont == null) {
-        largeFont = new Font(smallFont.FontFamily, smallFont.Size * 2, smallFont.Unit);
-      }
-
-      SetFont(largeFontToolStripMenuItem.Checked ? largeFont : smallFont);
-      //textBox1.Font = font;
-      //linkLabel1.Font = font;
-      //label1.Font = font;
-    }
-
-    public void SetFont(System.Drawing.Font font)
-    {
-      stateList.Font = font;
-      currentStateView.Font = font;
-      matchesList.Font = font;
-    }
-
-    private void Main_Load(object sender, EventArgs e)
-    {
-
-    }
-
-    private void currentStateView_KeyDown(object sender, KeyEventArgs e)
-    {
-      var node = SelectedNode();
-      if (node == null) return;
-
-      if (e.KeyCode == Keys.Right && !node.skel.Expanded && node.skel.Expandable) {
-        node.skel.Expanded = true;
-        SyncCurrentStateView();
-        return;
-      }
-
-      if (e.KeyCode == Keys.Left) {
-        if (node.skel.Expanded) {
-          node.skel.Expanded = false;
-          SyncCurrentStateView();
-          return;
-        } else {
-          var par = node.skel.parent;
-          if (par != null && par.parent != null) {
-            // par.Expanded = false;
-            foreach (DisplayItem it in currentStateView.Items) {
-              it.Selected = it.skel == par;
-              it.Focused = it.skel == par;
-              if (it.Selected) {
-                it.EnsureVisible();
-              }
-            }
-            SyncCurrentStateView();
-          }
-        }
-      }
-    }
-  }
-
-  internal class DisplayItem : ListViewItem
-  {
-    internal SkeletonItem skel;
-    internal int stateId;
-    internal bool active;
-    internal IDisplayNode dispNode;
-
-    public bool IsMatchListItem { get; set; }
-
-    internal void Set(SkeletonItem s, int id, int prevId)
-    {
-      if (skel == s && stateId == id)
-        return;
-      skel = s;
-      stateId = id;
-
-      dispNode = skel.displayNodes[stateId];
-      active = dispNode != null;
-
-      var closeStateId = stateId;
-
-      if (dispNode == null) {
-        while (closeStateId < skel.displayNodes.Length && skel.displayNodes[closeStateId] == null)
-          closeStateId++;
-        if (closeStateId >= skel.displayNodes.Length) {
-          closeStateId = stateId;
-          while (closeStateId >= 0 && skel.displayNodes[closeStateId] == null)
-            closeStateId--;
-        }
-        dispNode = skel.displayNodes[closeStateId];
-      }
-
-      var fullName = skel.LongName(closeStateId);
-      var tooltip = dispNode.ToolTip;
-      if (tooltip == null)
-        tooltip = "";
-      if(tooltip.Length > 0 && tooltip[tooltip.Length - 1] != '\n')
-        tooltip += "\n";
-      tooltip += "Full name: " + fullName;
-      if (tooltip != null) {
-        this.ToolTipText = tooltip;
-      }
-
-      var name = dispNode.Name;
-      if (name != dispNode.ShortName)
-      {
-        name = dispNode.ShortName;
-      }
-
-      if (IsMatchListItem) {
-        Util.Assert(active);
-        name = fullName;
-      }
-
-      this.SubItems[0].Text = name;
-      this.SubItems[1].Text = active ? dispNode.Value : "";
-
-      var prev = "";
-
-      if (!IsMatchListItem && prevId >= 0 && skel.displayNodes[prevId] != null) {
-        prev = skel.displayNodes[prevId].Value;
-      }
-
-      this.SubItems[2].Text = prev;
-    }
-
-    internal DisplayItem()
-       : base(new string[] { "", "", "" })
-    {
-    }
-
-    /*
-    static internal string AliasesAsString(IDisplayNode dn)
-    {
-      if (dn == null) return "";
-
-      var sb = new StringBuilder();
-      var canon = dn.CanonicalValue;
-      foreach (var n in dn.Aliases) {
-        if (n == canon)
-          continue;
-        sb.Append(n).Append(", ");
-        if (sb.Length > 300)
-          break;
-      }
-      if (sb.Length > 2) sb.Length -= 2;
-      return sb.ToString();
-    }
-     */
-  }
-}
+using System;
+using System.Collections.Generic;
+using System.ComponentModel;
+using System.Data;
+using System.Drawing;
+using System.Drawing.Drawing2D;
+using System.Linq;
+using System.Text;
+using System.Windows.Forms;
+
+using System.IO;
+using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie.ModelViewer
+{
+  public partial class Main : Form
+  {
+    SkeletonItem unfoldingRoot;
+    SkeletonItem[] allItems;
+    public int CurrentState, PreviousState = -1;
+    IState[] states;
+    internal ILanguageProvider langProvider;
+    public ILanguageSpecificModel LangModel;
+    ToolStripMenuItem[] viewItems;
+    Model currentModel;
+    Model[] allModels;
+    int modelId;
+    string lastModelFileName;
+    internal ViewOptions viewOpts = new ViewOptions();
+    Font smallFont, largeFont;
+    int lineHeight;
+
+    // TODO this should be dynamically loaded
+    IEnumerable<ILanguageProvider> Providers()
+    {
+      yield return BCT.Provider.Instance;
+      yield return Vcc.Provider.Instance;
+      yield return Dafny.Provider.Instance;
+      yield return Base.Provider.Instance;
+    }
+
+    public Main(string[] args, bool runAsHostedWindow = false)
+    {
+      InitializeComponent();
+
+      smallFont = stateList.Font;
+
+      if (runAsHostedWindow) {
+        this.fileToolStripMenuItem.Enabled = false;
+        this.fileToolStripMenuItem.Visible = false;
+      }
+
+      viewItems = new ToolStripMenuItem[] {
+        normalToolStripMenuItem,
+        expertToolStripMenuItem,
+        everythingToolStripMenuItem,
+        includeTheKitchenSinkToolStripMenuItem
+      };
+
+      var debugBreak = false;
+      string filename = null;
+
+      for (int i = 1; i < args.Length; i++) {
+        var arg = args[i];
+        if (arg == "/break" || arg == "-break")
+          debugBreak = true;
+        else
+          filename = arg;
+      }
+
+      if (debugBreak) {
+        System.Diagnostics.Debugger.Launch();
+      }
+
+      if (filename != null) {
+        var idx = filename.IndexOf(':');
+        if (idx > 0) {
+          modelId = int.Parse(filename.Substring(idx + 1));
+          filename = filename.Substring(0, idx);
+        }
+      }
+
+      this.ReadModels(filename, this.modelId);
+    }
+
+    private void SetWindowTitle(string fileName)
+    {
+      if (fileName == null) {
+        this.Text = "Boogie Verification Debugger";
+      } else {
+        this.Text = Path.GetFileName(fileName) + " - Boogie Verification Debugger";
+      }
+    }
+
+    public void ReadModel(string model, int setModelIdTo = 0)
+    {
+      Contract.Requires(model != null);
+
+      using (var rd = new StringReader(model))
+      {
+        allModels = Model.ParseModels(rd).ToArray();
+      }
+
+      AddAndLoadModel(setModelIdTo);
+    }
+
+    public void ReadModels(string modelFileName, int setModelIdTo)
+    {
+      this.lastModelFileName = modelFileName;
+      this.langProvider = Base.Provider.Instance;
+
+      if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {
+        using (var rd = File.OpenText(modelFileName)) {
+          allModels = Model.ParseModels(rd).ToArray();
+        }
+
+        AddAndLoadModel(setModelIdTo);
+      } else {
+        currentModel = new Model();
+      }
+
+      this.SetWindowTitle(modelFileName);
+    }
+
+    private void AddAndLoadModel(int setModelIdTo)
+    {
+      modelId = setModelIdTo;
+
+      if (modelId >= allModels.Length)
+        modelId = 0;
+
+      currentModel = allModels[modelId];
+      AddModelMenu();
+
+      foreach (var p in Providers())
+      {
+        if (p.IsMyModel(currentModel))
+        {
+          this.langProvider = p;
+          break;
+        }
+      }
+
+      LoadModel(modelId);
+    }
+
+    private void LoadModel(int idx)
+    {
+      var i = 0;
+
+      //var stateIdx = stateList.SelectedIndices.Count == 0 ? 0 : stateList.SelectedIndices[0];
+
+      modelId = idx;
+      foreach (ToolStripMenuItem it in modelsToolStripMenuItem.DropDownItems) {
+        it.Checked = i++ == idx;
+      }
+      currentModel = allModels[idx];
+      BuildModel();
+
+      /*
+      if (stateList.Items.Count <= stateIdx)
+        stateIdx = 0;
+      stateList.Items[stateIdx].Selected = true;      
+       */
+    }
+
+    private void AddModelMenu()
+    {
+      modelsToolStripMenuItem.DropDownItems.Clear();
+      var idx = 0;
+      foreach (var m in allModels) {
+        var currIdx = idx++; // this local needs to be in this block
+        var menuItem = modelsToolStripMenuItem.DropDownItems.Add(string.Format("Model #&{0}", currIdx), null, (s, a) => LoadModel(currIdx)) as ToolStripMenuItem;
+        if (currIdx <= 9) {
+          menuItem.ShortcutKeys = Keys.Control | (Keys)(currIdx + Keys.D0);
+        }
+      }
+    }
+
+    private void BuildModel()
+    {
+      stateList.Items.Clear();
+
+      var items = new List<ListViewItem>();
+      LangModel = langProvider.GetLanguageSpecificModel(currentModel, viewOpts);
+      states = LangModel.States.ToArray();
+      var oldRoot = unfoldingRoot;
+      SkeletonItem selectedSkel = null;
+      if (oldRoot != null && SelectedNode() != null) {
+        selectedSkel = SelectedNode().skel;
+      }
+      unfoldingRoot = new SkeletonItem(this, states.Length);
+      allItems = unfoldingRoot.PopulateRoot(states);
+
+      var idx = 0;
+      foreach (var i in states) {
+        var it = new ListViewItem(new string[] { idx.ToString(), i.Name, "" });
+        it.Tag = i;
+        items.Add(it);
+        idx++;
+      }
+      stateList.Items.AddRange(items.ToArray());
+      unfoldingRoot.Expanded = true;
+
+      if (oldRoot == null) {
+        SetState(0);
+        stateList.Items[0].Selected = true;
+        SetColumnSizes();
+      } else {
+        var mapping = new Dictionary<SkeletonItem, SkeletonItem>();
+        unfoldingRoot.SyncWith(mapping, oldRoot);
+        SkeletonItem newIt = null;
+        while (selectedSkel != null) {
+          if (mapping.TryGetValue(selectedSkel, out newIt)) break;
+          selectedSkel = selectedSkel.parent;
+        }
+        if (CurrentState >= stateList.Items.Count)
+          CurrentState = 0;
+        if (PreviousState >= stateList.Items.Count)
+          PreviousState = -1;
+        if (newIt != null) GotoNode(newIt);
+        SyncStateListValues();
+        UpdateMatches(true);
+      }
+    }
+
+    private void SetColumnSizes()
+    {
+      currentStateView.Columns[0].Width = currentStateView.Width - currentStateView.Columns[1].Width - currentStateView.Columns[2].Width - 25;
+      stateList.Columns[1].Width = stateList.Width - stateList.Columns[0].Width - stateList.Columns[2].Width - 25;
+    }
+
+    public void SetState(int id, bool updateView = false)
+    {
+      if (updateView)
+      {
+        stateList.SelectedIndices.Clear();
+        stateList.SelectedIndices.Add(id);
+      }
+      if (CurrentState != id) {
+        PreviousState = CurrentState;
+        CurrentState = id;
+      }
+      UpdateMatches(true);
+    }
+
+    public void HideStateList()
+    {
+      stateList.Hide();
+      splitContainer1.Panel2.Hide();
+      splitContainer1.Panel2Collapsed = true;
+      splitContainer1.SplitterDistance = splitContainer1.Width;
+    }
+
+    public void HideMenuStrip()
+    {
+      menuStrip1.Hide();
+    }
+
+    internal void Activate(TreeNode treeNode)
+    {
+      throw new NotImplementedException();
+    }
+
+    private void listBox1_SelectedIndexChanged(object sender, EventArgs e)
+    {
+
+    }
+
+    static Color Col(int c)
+    {
+      return Color.FromArgb(c >> 16, (c >> 8) & 0xff, c & 0xff);
+    }
+
+    static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };
+    static Pen plusPen = new Pen(Col(0xaaaaaa));
+    static Brush grayedOut = new SolidBrush(Col(0xaaaaaa));
+    static Brush nonPrimary = new SolidBrush(Col(0xeeeeee));
+    static Brush matchBg = new SolidBrush(Col(0xFFFA6F));
+
+    static SolidBrush currentStateBrush = new SolidBrush(Color.Red);
+    static SolidBrush regularStateBrush = new SolidBrush(Color.Black);
+    static SolidBrush previousStateBrush = new SolidBrush(Color.Blue);
+
+    static SolidBrush[] categoryBrushes = new SolidBrush[] {
+      new SolidBrush(Color.Black), // Local
+      new SolidBrush(Color.Black), // PhysField
+      new SolidBrush(Color.Green), // SpecField
+      new SolidBrush(Color.Peru), // MethodologyProperty
+      new SolidBrush(Color.Green), // UserFunction
+      new SolidBrush(Color.Black), // Maplet
+    };
+
+    private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)
+    {
+      var item = (DisplayItem)e.Item;
+      var skel = item.skel;
+      var rect = e.Bounds;
+      var listView = (ListView)sender;
+      lineHeight = rect.Height;
+      rect.Y += 1;
+      rect.Height -= 2;
+
+      var textBrush = Brushes.Black;
+      if (listView.SelectedIndices.Count > 0 && listView.SelectedIndices[0] == e.ItemIndex) {
+        e.Graphics.FillRectangle(Brushes.Aquamarine, rect);
+        textBrush = Brushes.White;
+      } else {
+        var bg = Brushes.White;
+        if (item.active && !skel.isPrimary[CurrentState])
+          bg = nonPrimary;
+        if (item.skel.isMatch)
+          bg = matchBg;
+        e.Graphics.FillRectangle(bg, rect);
+      }
+
+      var off = lineHeight * item.skel.level;
+      if (item.IsMatchListItem)
+        off = 0;
+
+      {
+        var plusRect = rect;
+        plusRect.Width = lineHeight;
+        plusRect.X += off;
+        var plusBorder = plusRect;
+        plusBorder.Height = lineHeight / 2;
+        plusBorder.Width = lineHeight / 2;
+        plusBorder.X += lineHeight / 4;
+        plusBorder.Y += lineHeight / 4;
+        e.Graphics.DrawRectangle(plusPen, plusBorder);
+        if (skel.Expandable) {
+          float midX = plusBorder.X + plusBorder.Width / 2;
+          float midY = plusBorder.Y + plusBorder.Height / 2;
+          e.Graphics.DrawLine(plusPen, plusBorder.X + 2, midY, plusBorder.Right - 2, midY);
+          if (!item.skel.expanded)
+            e.Graphics.DrawLine(plusPen, midX, plusBorder.Y + 2, midX, plusBorder.Bottom - 2);
+        }
+      }
+
+      off += lineHeight + 3;
+      var nameRect = rect;
+      var font = listView.Font;
+
+      textBrush = categoryBrushes[(int)item.dispNode.Category];
+
+      if (!item.active)
+        textBrush = grayedOut;
+
+      nameRect.Width = listView.Columns[0].Width - 1 - off;
+      nameRect.X += off;
+      var width = DrawString(e.Graphics, item.SubItems[0].Text, font, textBrush, nameRect);
+
+      textBrush = item.active ? Brushes.Black : grayedOut;
+      nameRect.X += width + 4;
+      nameRect.Width = listView.Columns[0].Width + listView.Columns[1].Width - nameRect.X;
+      width = DrawString(e.Graphics, item.SubItems[1].Text, font, textBrush, nameRect);
+
+      nameRect.X += width + 4;
+      nameRect.Width = listView.Width - nameRect.X;
+      var t = item.SubItems[2].Text;
+      width = DrawString(e.Graphics, t, font, t == item.SubItems[1].Text ? grayedOut : Brushes.Black, nameRect);
+    }
+
+    private int DrawString(Graphics g, string s, Font font, Brush textBrush, Rectangle minRect)
+    {
+      var sz = g.MeasureString(s, font).Width;
+      if (sz > minRect.Width - 2) {
+        minRect.Width = (int)(sz + 20);
+      }
+      g.DrawString(s, font, textBrush, minRect);
+      return minRect.Width;
+    }
+
+    private void listView1_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e)
+    {
+      e.DrawBackground();
+      var brush = regularStateBrush;
+      if (e.Header.Index == 1)
+        brush = currentStateBrush;
+      else if (e.Header.Index == 2)
+        brush = previousStateBrush;
+
+      Rectangle r = e.Bounds;
+      r.X += 5;
+      r.Y += 4;
+      DrawString(e.Graphics, e.Header.Text, e.Header.ListView.Font, brush, r);
+    }
+
+    private void listView1_MouseUp(object sender, MouseEventArgs e)
+    {
+      var clickedItem = (DisplayItem)currentStateView.GetItemAt(5, e.Y);
+      if (clickedItem != null) {
+        clickedItem.Selected = true;
+        clickedItem.Focused = true;
+
+        var skel = clickedItem.skel;
+        int plusLoc = skel.level * lineHeight;
+        if (skel.Expandable && e.X >= plusLoc && e.X <= plusLoc + lineHeight) {
+          skel.Expanded = !skel.Expanded;
+          SyncCurrentStateView();
+        }
+      }
+    }
+
+    private void SyncCurrentStateView()
+    {
+      SyncListView(unfoldingRoot.RecChildren, currentStateView, (x, y) => { });
+    }
+
+    private void SyncListView(IEnumerable<SkeletonItem> items, ListView listView, Action<DisplayItem, SkeletonItem> cb)
+    {
+      var ch = items.ToArray();
+      var missing = ch.Length - listView.Items.Count;
+      listView.BeginUpdate();
+      if (missing < 0) {
+        missing = -missing;
+        while (missing-- > 0) {
+          listView.Items.RemoveAt(listView.Items.Count - 1);
+        }
+      } else {
+        while (missing-- > 0) {
+          listView.Items.Add(new DisplayItem());
+        }
+      }
+      for (int i = 0; i < ch.Length; ++i) {
+        var di = (DisplayItem)listView.Items[i];
+        cb(di, ch[i]);
+        di.Set(ch[i], CurrentState, PreviousState);
+      }
+      listView.EndUpdate();
+      listView.Invalidate();
+    }
+
+    private void listView1_ColumnWidthChanged(object sender, ColumnWidthChangedEventArgs e)
+    {
+      currentStateView.Invalidate();
+    }
+
+    private void listView1_Resize(object sender, EventArgs e)
+    {
+      SetColumnSizes();
+      currentStateView.Invalidate();
+    }
+
+    private void stateList_SelectedIndexChanged(object sender, EventArgs e)
+    {
+      if (stateList.SelectedItems.Count == 0) return;
+      var sel = stateList.SelectedItems[0].Index;
+
+      if (PreviousState >= 0)
+        stateList.Items[PreviousState].ForeColor = regularStateBrush.Color;
+
+      SetState(sel);
+    }
+
+    DisplayItem SelectedNode()
+    {
+      if (currentStateView.SelectedItems.Count == 0) return null;
+      return (DisplayItem)currentStateView.SelectedItems[0];
+    }
+
+    private void currentStateView_SelectedIndexChanged(object sender, EventArgs e)
+    {
+      SyncStateListValues();
+    }
+
+    private void SyncStateListValues()
+    {
+      var sel = SelectedNode();
+      if (sel == null) return;
+
+      stateList.BeginUpdate();
+      for (int i = 0; i < sel.skel.displayNodes.Length; ++i) {
+        var dn = sel.skel.displayNodes[i];
+        stateList.Items[i].SubItems[2].Text = dn == null ? "" : dn.Value;
+      }
+      stateList.EndUpdate();
+    }
+
+    private void ExpandParents(SkeletonItem item)
+    {
+      item = item.parent;
+      while (item != null) {
+        item.Expanded = true;
+        item = item.parent;
+      }
+    }
+
+    private void textBox1_TextChanged(object sender, EventArgs e)
+    {
+      UpdateMatches(false);
+    }
+
+    private void UpdateMatches(bool force)
+    {
+      var bad = false;
+      Model.Element eltEq = null;
+      var eltRef = new List<Model.Element>();
+      var words = new List<string>();
+
+      foreach (var w in textBox1.Text.Split(' ')) {
+        if (w == "") continue;
+        if (w.StartsWith("eq:")) {
+          if (eltEq != null) bad = true;
+          else {
+            eltEq = LangModel.FindElement(w.Substring(3));
+            if (eltEq == null) bad = true;
+          }
+        } else if (w.StartsWith("use:")) {
+          var e = LangModel.FindElement(w.Substring(4));
+          if (e == null) bad = true;
+          else eltRef.Add(e);
+        } else {
+          words.Add(w.ToLower());
+        }
+      }
+
+      textBox1.ForeColor = bad ? Color.Red : Color.Black;
+
+      var wordsA = words.ToArray();
+      var refsA = eltRef.ToArray();
+
+      if (eltEq == null && wordsA.Length == 0 && refsA.Length == 0)
+        bad = true;
+
+      var changed = true; // force;
+      var matches = new List<SkeletonItem>();
+
+      foreach (var s in allItems) {
+        var newMatch = false;
+        if (s.isPrimary[CurrentState] && !bad) {
+          newMatch = s.MatchesWords(wordsA, refsA, eltEq, CurrentState);
+        }
+        if (newMatch)
+          matches.Add(s);
+        if (s.isMatch != newMatch) {
+          changed = true;
+          s.isMatch = newMatch;
+        }
+      }
+
+      if (PreviousState >= 0)
+        stateList.Items[PreviousState].ForeColor = previousStateBrush.Color;
+      stateList.Items[CurrentState].ForeColor = currentStateBrush.Color;
+
+      if (changed) {
+        SyncListView(matches, matchesList, (di, _) => { di.IsMatchListItem = true; });
+        SyncCurrentStateView();
+      }
+    }
+
+    private void matchesList_Resize(object sender, EventArgs e)
+    {
+      matchesList.Invalidate();
+    }
+
+    private void matchesList_DoubleClick(object sender, EventArgs e)
+    {
+      if (matchesList.SelectedItems.Count == 0) return;
+      var sel = (DisplayItem)matchesList.SelectedItems[0];
+      GotoNode(sel.skel);
+    }
+
+    private void linkLabel1_LinkClicked(object sender, LinkLabelLinkClickedEventArgs e)
+    {
+      foreach (DisplayItem it in matchesList.Items) {
+        ExpandParents(it.skel);
+      }
+      SyncCurrentStateView();
+    }
+
+    private void SetSearch(string text)
+    {
+      textBox1.Text = text;
+    }
+
+    private void GotoNode(SkeletonItem skel)
+    {
+      ExpandParents(skel);
+      SyncCurrentStateView();
+      foreach (DisplayItem it in currentStateView.Items) {
+        if (it.skel == skel) {
+          it.Selected = true;
+          currentStateView.EnsureVisible(it.Index);
+          break;
+        }
+      }
+    }
+
+    private IEnumerable<SkeletonItem> NamesFor(Model.Element elt)
+    {
+      var words = new string[0];
+      var elts = new Model.Element[0];
+
+      foreach (var s in allItems) {
+        if (s.isPrimary[CurrentState] && s.MatchesWords(words, elts, elt, CurrentState)) {
+          yield return s;
+        }
+      }
+    }
+
+    private void AddMenuItems(IEnumerable<SkeletonItem> skels, ToolStripItemCollection items, string pref, int max)
+    {
+      var skelsM = skels.Take(max).ToArray();
+
+      foreach (var s in skelsM) {
+        var tmp = s;
+        items.Add(pref + s.LongName(CurrentState), null, (x, _) => GotoNode(tmp));
+      }
+
+      if (skelsM.Length == max)
+        items.Add(new ToolStripMenuItem("...") { Enabled = false });
+    }
+
+    private void stateViewMenu_Opening(object sender, CancelEventArgs e)
+    {
+      IDisplayNode sel = null;
+      SkeletonItem skel = null;
+      if (SelectedNode() != null) {
+        sel = SelectedNode().dispNode;
+        skel = SelectedNode().skel;
+      }
+
+      var items = stateViewMenu.Items;
+      items.Clear();
+
+      if (sel == null) {
+        items.Add(new ToolStripMenuItem("Unavailable") { Enabled = false });
+        return;
+      }
+
+      foreach (var x in sel.References.Where(q => q != sel.Element)) {
+        var t = new ToolStripMenuItem(LangModel.CanonicalName(x));
+        items.Add(t);
+        AddMenuItems(NamesFor(x), t.DropDownItems, "= ", 20);
+      }
+
+      if (sel.Element != null) {
+        var selName = LangModel.CanonicalName(sel.Element);
+        items.Add("Find uses...", null, (s, _) => SetSearch("use:" + selName));
+
+        var aliases = NamesFor(sel.Element).Where(s => s != skel).ToArray();
+        if (aliases.Length > 0) {
+          items.Add("Aliases...", null, (s, _) => SetSearch("eq:" + selName));
+          AddMenuItems(aliases, items, "   = ", 10);
+        }
+      }
+    }
+
+    private void normalToolStripMenuItem_Click(object sender, EventArgs e)
+    {
+      int viewLev = -1;
+      for (int i = 0; i < viewItems.Length; ++i) {
+        if (viewItems[i] == sender) {
+          viewLev = i;
+          viewItems[i].Checked = true;
+        } else {
+          viewItems[i].Checked = false;
+        }
+      }
+      if (viewLev != -1 && viewLev != viewOpts.ViewLevel) {
+        viewOpts.ViewLevel = viewLev;
+        BuildModel();
+      }
+    }
+
+    private void debugToolStripMenuItem_Click(object sender, EventArgs e)
+    {
+      debugToolStripMenuItem.Checked = !debugToolStripMenuItem.Checked;
+      viewOpts.DebugMode = debugToolStripMenuItem.Checked;
+      BuildModel();
+    }
+
+    private void exitToolStripMenuItem_Click(object sender, EventArgs e)
+    {
+      this.Close();
+    }
+
+    private void reloadModelFileToolStripMenuItem_Click(object sender, EventArgs e)
+    {
+      ReadModels(this.lastModelFileName, this.modelId);
+    }
+
+    private SourceView sourceView;
+    private void ShowSource()
+    {
+      if (stateList.SelectedItems.Count == 0) return;
+      var li = stateList.SelectedItems[0] as ListViewItem;
+      if (li != null) {
+        var r = ((IState)li.Tag).ShowSource();
+        if (r != null) {
+          if (sourceView == null) {
+            sourceView = new SourceView();
+          }
+          sourceView.largeFont = largeFontToolStripMenuItem.Checked;
+          sourceView.SetSourceLocation(r);
+          sourceView.BringToFront();
+        }
+      }
+    }
+
+    private void showSourceToolStripMenuItem_Click(object sender, EventArgs e)
+    {
+      ShowSource();
+    }
+
+    private void stateList_DoubleClick(object sender, EventArgs e)
+    {
+      ShowSource();
+    }
+
+    private void openModelMenuItem_Click(object sender, EventArgs e)
+    {
+      if (this.openModelFileDialog.ShowDialog() == System.Windows.Forms.DialogResult.OK) {
+        this.ReadModels(this.openModelFileDialog.FileName, 0);
+      }
+    }
+
+    private void largeFontToolStripMenuItem_Click(object sender, EventArgs e)
+    {
+      largeFontToolStripMenuItem.Checked = !largeFontToolStripMenuItem.Checked;
+
+      if (largeFont == null) {
+        largeFont = new Font(smallFont.FontFamily, smallFont.Size * 2, smallFont.Unit);
+      }
+
+      SetFont(largeFontToolStripMenuItem.Checked ? largeFont : smallFont);
+      //textBox1.Font = font;
+      //linkLabel1.Font = font;
+      //label1.Font = font;
+    }
+
+    public void SetFont(System.Drawing.Font font)
+    {
+      stateList.Font = font;
+      currentStateView.Font = font;
+      matchesList.Font = font;
+    }
+
+    private void Main_Load(object sender, EventArgs e)
+    {
+
+    }
+
+    private void currentStateView_KeyDown(object sender, KeyEventArgs e)
+    {
+      var node = SelectedNode();
+      if (node == null) return;
+
+      if (e.KeyCode == Keys.Right && !node.skel.Expanded && node.skel.Expandable) {
+        node.skel.Expanded = true;
+        SyncCurrentStateView();
+        return;
+      }
+
+      if (e.KeyCode == Keys.Left) {
+        if (node.skel.Expanded) {
+          node.skel.Expanded = false;
+          SyncCurrentStateView();
+          return;
+        } else {
+          var par = node.skel.parent;
+          if (par != null && par.parent != null) {
+            // par.Expanded = false;
+            foreach (DisplayItem it in currentStateView.Items) {
+              it.Selected = it.skel == par;
+              it.Focused = it.skel == par;
+              if (it.Selected) {
+                it.EnsureVisible();
+              }
+            }
+            SyncCurrentStateView();
+          }
+        }
+      }
+    }
+  }
+
+  internal class DisplayItem : ListViewItem
+  {
+    internal SkeletonItem skel;
+    internal int stateId;
+    internal bool active;
+    internal IDisplayNode dispNode;
+
+    public bool IsMatchListItem { get; set; }
+
+    internal void Set(SkeletonItem s, int id, int prevId)
+    {
+      if (skel == s && stateId == id)
+        return;
+      skel = s;
+      stateId = id;
+
+      dispNode = skel.displayNodes[stateId];
+      active = dispNode != null;
+
+      var closeStateId = stateId;
+
+      if (dispNode == null) {
+        while (closeStateId < skel.displayNodes.Length && skel.displayNodes[closeStateId] == null)
+          closeStateId++;
+        if (closeStateId >= skel.displayNodes.Length) {
+          closeStateId = stateId;
+          while (closeStateId >= 0 && skel.displayNodes[closeStateId] == null)
+            closeStateId--;
+        }
+        dispNode = skel.displayNodes[closeStateId];
+      }
+
+      var fullName = skel.LongName(closeStateId);
+      var tooltip = dispNode.ToolTip;
+      if (tooltip == null)
+        tooltip = "";
+      if(tooltip.Length > 0 && tooltip[tooltip.Length - 1] != '\n')
+        tooltip += "\n";
+      tooltip += "Full name: " + fullName;
+      if (tooltip != null) {
+        this.ToolTipText = tooltip;
+      }
+
+      var name = dispNode.Name;
+      if (name != dispNode.ShortName)
+      {
+        name = dispNode.ShortName;
+      }
+
+      if (IsMatchListItem) {
+        Util.Assert(active);
+        name = fullName;
+      }
+
+      this.SubItems[0].Text = name;
+      this.SubItems[1].Text = active ? dispNode.Value : "";
+
+      var prev = "";
+
+      if (!IsMatchListItem && prevId >= 0 && skel.displayNodes[prevId] != null) {
+        prev = skel.displayNodes[prevId].Value;
+      }
+
+      this.SubItems[2].Text = prev;
+    }
+
+    internal DisplayItem()
+       : base(new string[] { "", "", "" })
+    {
+    }
+
+    /*
+    static internal string AliasesAsString(IDisplayNode dn)
+    {
+      if (dn == null) return "";
+
+      var sb = new StringBuilder();
+      var canon = dn.CanonicalValue;
+      foreach (var n in dn.Aliases) {
+        if (n == canon)
+          continue;
+        sb.Append(n).Append(", ");
+        if (sb.Length > 300)
+          break;
+      }
+      if (sb.Length > 2) sb.Length -= 2;
+      return sb.ToString();
+    }
+     */
+  }
+}
-- 
cgit v1.2.3