diff options
author | Dan Rosén <danr@chalmers.se> | 2014-06-24 10:32:15 -0700 |
---|---|---|
committer | Dan Rosén <danr@chalmers.se> | 2014-06-24 10:32:15 -0700 |
commit | 3f2958db79781cc73938c4e9ed9ba92efcf66f62 (patch) | |
tree | 48e678df24ccf700780379a2f737e80625f4235c /Source/Core/AbsyExpr.cs | |
parent | 98bcde1368eb6a5df44cf252e3a2f8d8f509a0df (diff) |
Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"
When running boogie form the command line, this should be on by default.
On the other hand, the TokenTextWriter constructors and PrintBplFile now have an
argument for this, but by default it is off.
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
-rw-r--r-- | Source/Core/AbsyExpr.cs | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 70b445b1..d6dd17c9 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1418,15 +1418,18 @@ namespace Microsoft.Boogie { bool parensNeeded = opBS < ctxtBS ||
(opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
+ var pop = stream.push(FunctionName);
if (parensNeeded) {
stream.Write("(");
}
cce.NonNull(args[0]).Emit(stream, opBindingStrength, fragileLeftContext);
+ stream.sep();
stream.Write(" {0} ", FunctionName);
cce.NonNull(args[1]).Emit(stream, opBindingStrength, fragileRightContext);
if (parensNeeded) {
stream.Write(")");
}
+ stream.pop(pop);
}
public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
//Contract.Requires(subjectForErrorReporting != null);
@@ -2521,13 +2524,17 @@ namespace Microsoft.Boogie { //Contract.Requires(args != null);
stream.SetToken(ref this.tok);
Contract.Assert(args.Count == 3);
- stream.Write("(if ");
+ stream.push();
+ stream.Write("(if ");
cce.NonNull(args[0]).Emit(stream, 0x00, false);
+ stream.sep();
stream.Write(" then ");
cce.NonNull(args[1]).Emit(stream, 0x00, false);
+ stream.sep();
stream.Write(" else ");
cce.NonNull(args[2]).Emit(stream, 0x00, false);
stream.Write(")");
+ stream.pop();
}
public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
|