summaryrefslogtreecommitdiff
path: root/Source/Dafny/Printer.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Printer.cs')
-rw-r--r--Source/Dafny/Printer.cs14
1 files changed, 6 insertions, 8 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6ec05a50..5eba44ee 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -403,19 +403,14 @@ namespace Microsoft.Dafny {
}
}
- public void PrintAttributeArgs(List<Attributes.Argument> args, bool isFollowedBySemicolon) {
+ public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {
Contract.Requires(args != null);
string prefix = " ";
- foreach (Attributes.Argument arg in args) {
+ foreach (var arg in args) {
Contract.Assert(arg != null);
wr.Write(prefix);
prefix = ", ";
- if (arg.S != null) {
- wr.Write("\"{0}\"", arg.S);
- } else {
- Contract.Assert( arg.E != null);
- PrintExpression(arg.E, isFollowedBySemicolon);
- }
+ PrintExpression(arg, isFollowedBySemicolon);
}
}
@@ -1219,6 +1214,9 @@ namespace Microsoft.Dafny {
wr.Write("null");
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is string) {
+ var str = (StringLiteralExpr)e;
+ wr.Write("{0}\"{1}\"", str.IsVerbatim ? "@" : "", (string)e.Value);
} else if (e.Value is Basetypes.BigDec) {
Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;
wr.Write((dec.Mantissa >= 0) ? "" : "-");