Now the parser parses "Type" rather than "IToken" for a trait

1 files changed, 9 insertions, 9 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f990f9ff..dd1ff730 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -465,7 +465,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/*!*/>();

@@ -482,15 +482,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 		if (la.kind == 31) {

 			Get();

-			QualifiedName(out traitId);

+			Type(out trait);

 		}

 		Expect(15);

-		bodyStart = t; 

+		bodyStart = t;  

 		while (StartOf(2)) {

 			ClassMemberDecl(members, true);

 		}

 		Expect(16);

-		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;

 		

@@ -837,6 +837,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Expect(47);

 	}

 

+	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;

@@ -1164,11 +1169,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);