summaryrefslogtreecommitdiff
path: root/Source/Dafny/Parser.cs
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-11-06 14:40:17 -0800
committerGravatar leino <unknown>2014-11-06 14:40:17 -0800
commit4b8346cdb84df7ba1bdd59aca41c6e7807f912c8 (patch)
treecf0ffa9997b1f01d93a432da9948b1ef679e2f65 /Source/Dafny/Parser.cs
parent41ae0ef413e2806e1ee753f56de2152938902fac (diff)
parentfd15838d416860cd7fe9e5303fb4d624d0b82ab3 (diff)
Merge
Diffstat (limited to 'Source/Dafny/Parser.cs')
-rw-r--r--Source/Dafny/Parser.cs18
1 files changed, 9 insertions, 9 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 5135712d..d710b72b 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -466,7 +466,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
- List<IToken>/*!*/ traitId=null;
+ Type/*!*/ trait = null;
Attributes attrs = null;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
@@ -483,15 +483,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
if (la.kind == 36) {
Get();
- QualifiedName(out traitId);
+ Type(out trait);
}
Expect(20);
- bodyStart = t;
+ bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, true);
}
Expect(21);
- c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -838,6 +838,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Expect(52);
}
+ void Type(out Type ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
+ TypeAndToken(out tok, out ty);
+ }
+
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
@@ -1165,11 +1170,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
}
- void Type(out Type ty) {
- Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
- TypeAndToken(out tok, out ty);
- }
-
void Expression(out Expression e, bool allowSemi, bool allowLambda) {
Expression e0; IToken endTok;
EquivExpression(out e, allowSemi, allowLambda);