Updated parser generation to work with latest update in boogiepartners. Note that Coco.exe is now included in boogiepartners.

1 files changed, 14 insertions, 15 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index dae1b95e..b4f45159 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -78,11 +78,11 @@ public class Parser {
 	const bool _x = false;

 	const int minErrDist = 2;

 

-	public Scanner/*!*/ scanner;

-	public Errors/*!*/  errors;

+	public Scanner scanner;

+	public Errors  errors;

 

-	public Token/*!*/ t;    // last recognized token

-	public Token/*!*/ la;   // lookahead token

+	public Token t;    // last recognized token

+	public Token la;   // lookahead token

 	int errDist = minErrDist;

 

 readonly Expression/*!*/ dummyExpr;

@@ -454,10 +454,10 @@ bool IsType(ref IToken pt) {
 /*--------------------------------------------------------------------------*/

 

 

-	public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {

+	public Parser(Scanner scanner, Errors errors) {

 		this.scanner = scanner;

 		this.errors = errors;

-		Token/*!*/ tok = new Token();

+		Token tok = new Token();

 		tok.val = "";

 		this.la = tok;

 		this.t = new Token(); // just to satisfy its non-null constraint

@@ -468,13 +468,13 @@ bool IsType(ref IToken pt) {
 		errDist = 0;

 	}

 

-	public void SemErr (string/*!*/ msg) {

+	public void SemErr (string msg) {

 		Contract.Requires(msg != null);

 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

 

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+	public void SemErr(IToken tok, string msg) {

 	  Contract.Requires(tok != null);

 	  Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

@@ -4385,10 +4385,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Dafny();

 		Expect(0);

 

-		Expect(0);

 	}

 

-	static readonly bool[,]/*!*/ set = {

+	static readonly bool[,] set = {

 		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_T, _x,_x,_T,_T, _T,_x,_x,_T, _T,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_x,_T, _T,_T,_x,_x, _T,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_x,_x,_x},

 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _T,_x,_x,_x, _x,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},

 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},

@@ -4428,7 +4427,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 public class Errors {

 	public int count = 0;                                    // number of errors detected

-	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

+	public System.IO.TextWriter errorStream = Console.Out;   // error messages go to this stream

 	public string errMsgFormat = "{0}({1},{2}): Error: {3}"; // 0=filename, 1=line, 2=column, 3=text

 	public string warningMsgFormat = "{0}({1},{2}): Warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

 

@@ -4436,7 +4435,7 @@ public class Errors {
 		SynErr(filename, line, col, GetSyntaxErrorString(n));

 	}

 

-	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

+	public virtual void SynErr(string filename, int line, int col, string msg) {

 		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);

 		count++;

@@ -4693,19 +4692,19 @@ public class Errors {
 		return s;

 	}

 

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

+	public void SemErr(IToken tok, string msg) {  // semantic errors

 		Contract.Requires(tok != null);

 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

 

-	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

+	public virtual void SemErr(string filename, int line, int col, string msg) {

 		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);

 		count++;

 	}

 

-	public void Warning(IToken/*!*/ tok, string/*!*/ msg) {  // warnings

+	public void Warning(IToken tok, string msg) {  // warnings

 		Contract.Requires(tok != null);

 		Contract.Requires(msg != null);

 		Warning(tok.filename, tok.line, tok.col, msg);