summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-16 18:12:56 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-16 18:12:56 -0700
commit8dc1aa7a1e0d6e61fb2c24191d8305d222f8da88 (patch)
tree2597205685898a28fb2255cf4ee7aa46b8fe730e /Util
parent94eb01be99a3273796fe36e631740be1c69163f3 (diff)
DafnyExtension: various improvements
Diffstat (limited to 'Util')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs55
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs2
2 files changed, 38 insertions, 19 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 0304dd20..bc35e33c 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -119,7 +119,7 @@ namespace DafnyLanguage
foreach (var ctor in dt.Ctors) {
foreach (var dtor in ctor.Destructors) {
if (dtor != null) {
- newRegions.Add(new IdRegion(dtor.tok, dtor, "destructor", true));
+ IdRegion.Add(newRegions, dtor.tok, dtor, "destructor", true);
}
}
}
@@ -129,7 +129,7 @@ namespace DafnyLanguage
if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
- newRegions.Add(new IdRegion(p.tok, p, true));
+ IdRegion.Add(newRegions, p.tok, p, true);
}
f.Req.ForEach(e => ExprRegions(e, newRegions));
f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true));
@@ -141,10 +141,10 @@ namespace DafnyLanguage
} else if (member is Method) {
var m = (Method)member;
foreach (var p in m.Ins) {
- newRegions.Add(new IdRegion(p.tok, p, true));
+ IdRegion.Add(newRegions, p.tok, p, true);
}
foreach (var p in m.Outs) {
- newRegions.Add(new IdRegion(p.tok, p, true));
+ IdRegion.Add(newRegions, p.tok, p, true);
}
m.Req.ForEach(e => ExprRegions(e.E, newRegions));
m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true));
@@ -155,7 +155,7 @@ namespace DafnyLanguage
}
} else if (member is Field) {
var fld = (Field)member;
- newRegions.Add(new IdRegion(fld.tok, fld, "field", true));
+ IdRegion.Add(newRegions, fld.tok, fld, "field", true);
}
}
}
@@ -174,7 +174,7 @@ namespace DafnyLanguage
ExprRegions(fe.E, regions);
}
if (fe.Field != null) {
- regions.Add(new IdRegion(fe.tok, fe.Field, "field", false));
+ IdRegion.Add(regions, fe.tok, fe.Field, "field", false);
}
}
@@ -183,19 +183,19 @@ namespace DafnyLanguage
Contract.Requires(regions != null);
if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
- regions.Add(new IdRegion(e.tok, e.Var, false));
+ IdRegion.Add(regions, e.tok, e.Var, false);
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
- regions.Add(new IdRegion(e.tok, e.Field, "field", false));
+ IdRegion.Add(regions, e.tok, e.Field, "field", false);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
- regions.Add(new IdRegion(bv.tok, bv, true));
+ IdRegion.Add(regions, bv.tok, bv, true);
}
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
foreach (var kase in e.Cases) {
- kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
}
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
@@ -215,7 +215,7 @@ namespace DafnyLanguage
var s = (VarDeclStmt)stmt;
// Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's)
foreach (var lhs in s.Lhss) {
- regions.Add(new IdRegion(lhs.Tok, lhs, true));
+ IdRegion.Add(regions, lhs.Tok, lhs, true);
}
if (s.Update is UpdateStmt) {
var upd = (UpdateStmt)s.Update;
@@ -232,14 +232,14 @@ namespace DafnyLanguage
return;
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
- regions.Add(new IdRegion(s.Tok, s, true));
+ IdRegion.Add(regions, s.Tok, s, true);
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
- s.BoundVars.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
- kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true));
}
} else if (stmt is LoopStmt) {
var s = (LoopStmt)stmt;
@@ -261,7 +261,26 @@ namespace DafnyLanguage
public readonly int Length;
public readonly string HoverText;
public readonly bool IsDefinition;
- public IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) {
+
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition) {
+ Contract.Requires(regions != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(v != null);
+ if (!(tok is AutoGeneratedToken)) {
+ regions.Add(new IdRegion(tok, v, isDefinition));
+ }
+ }
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
+ Contract.Requires(regions != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(kind != null);
+ if (!(tok is AutoGeneratedToken)) {
+ regions.Add(new IdRegion(tok, decl, kind, isDefinition));
+ }
+ }
+
+ private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) {
Contract.Requires(tok != null);
Contract.Requires(v != null);
Start = tok.pos;
@@ -275,16 +294,16 @@ namespace DafnyLanguage
var formal = (Formal)v;
kind = formal.InParam ? "in-parameter" : "out-parameter";
}
- HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.ToString(), v.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(null/*TODO: use context*/), v.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
- public IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
+ private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition) {
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
Start = tok.pos;
Length = decl.Name.Length;
- HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullName, decl.Type.ToString(), decl.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullName, decl.Type.TypeName(null/*TODO: use context*/), decl.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index ff1159ec..34dcce3c 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -30,7 +30,7 @@ namespace DafnyLanguage
}
System.Windows.Shapes.Rectangle sh = new Rectangle() {
- Fill = dtag.Val == 0 ? Brushes.Goldenrod : Brushes.DarkOrange,
+ Fill = dtag.Val == 0 ? new SolidColorBrush(Color.FromRgb(255, 238, 98)) : Brushes.DarkOrange,
Height = 18.0,
Width = 3.0
};