diff options
author | 2010-11-06 01:21:11 +0000 | |
---|---|---|
committer | 2010-11-06 01:21:11 +0000 | |
commit | 6f9978cce118489f6f76d8c08321bae2b599d4e1 (patch) | |
tree | 4aacec933d45ce6cda817f76be9521da98135c52 /Source/ModelViewer/Main.cs | |
parent | 2538b1f5708027a85b9a3857d94c9d53648bcc3b (diff) |
Add find find uses and find aliases facilities
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 38 |
1 files changed, 34 insertions, 4 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index e8a9df36..5bc18fb2 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -27,7 +27,7 @@ namespace Microsoft.Boogie.ModelViewer IEnumerable<ILanguageProvider> Providers()
{
yield return Vcc.Provider.Instance;
- //yield return Dafny.Provider.Instance;
+ yield return Dafny.Provider.Instance;
yield return Base.Provider.Instance;
}
@@ -302,13 +302,43 @@ namespace Microsoft.Boogie.ModelViewer private void UpdateMatches(bool force)
{
- var words = textBox1.Text.Split(' ').Where(s => s != "").Select(s => s.ToLower()).ToArray();
+ 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("ref:")) {
+ 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 = force;
var matches = new List<SkeletonItem>();
+
foreach (var s in allItems) {
var newMatch = false;
- if (s.isPrimary[currentState] && words.Length > 0) {
- newMatch = s.MatchesWords(words, currentState);
+ if (s.isPrimary[currentState] && !bad) {
+ newMatch = s.MatchesWords(wordsA, refsA, eltEq, currentState);
}
if (newMatch)
matches.Add(s);
|