Minor change to grammar to avoid missing token

3 files changed, 17 insertions, 6 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 45018cd3..9dee1cc9 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1147,7 +1147,7 @@ TypeAndToken<out IToken tok, out Type ty>
                                          ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), dims == 0 ? null : tupleArgTypes);

                                        }

                                     .)

-  | (. Expression e; .)

+  | (. Expression e; tok = t; .)

     NameSegmentForTypeName<out e>

     { "." ident                      (. tok = t; List<Type> typeArgs = null; .)

       [ (. typeArgs = new List<Type>(); .)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ffe3f7f2..d0bcef21 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1609,7 +1609,7 @@ bool IsType(ref IToken pt) {
 			break;

 		}

 		case 1: {

-			Expression e; 

+			Expression e; tok = t; 

 			NameSegmentForTypeName(out e);

 			while (la.kind == 24) {

 				Get();

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index bdcddb70..c9c163e6 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -217,7 +217,7 @@ public class Scanner {
 

 	[ContractInvariantMethod]

 	void objectInvariant(){

-		Contract.Invariant(buffer!=null);

+		Contract.Invariant(this._buffer != null);

 		Contract.Invariant(t != null);

 		Contract.Invariant(start != null);

 		Contract.Invariant(tokens != null);

@@ -227,7 +227,18 @@ public class Scanner {
 		Contract.Invariant(errorHandler != null);

 	}

 

-	public Buffer/*!*/ buffer; // scanner buffer

+	private Buffer/*!*/ _buffer; // scanner buffer

+

+	public Buffer/*!*/ buffer {

+		get {

+			Contract.Ensures(Contract.Result<Buffer>() != null);

+			return this._buffer;

+		}

+		set {

+			Contract.Requires(value != null);

+			this._buffer = value;

+		}

+	}

 

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

@@ -307,7 +318,7 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

-			buffer = new Buffer(stream, false);

+			this._buffer = new Buffer(stream, false);

 			Filename = useBaseName? GetBaseName(fileName): fileName;

 			Init();

 		} catch (IOException) {

@@ -322,7 +333,7 @@ public class Scanner {
 	  Contract.Requires(fileName != null);

 		pt = tokens = new Token();  // first token is a dummy

 		t = new Token(); // dummy because t is a non-null field

-		buffer = new Buffer(s, true);

+		this._buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

 		Init();