diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-05 17:57:40 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-05 17:57:40 -0700 |
| commit | a1a041f3549cb1665964d30b666c825767d59afb (patch) | |
| tree | c0d06edd42a894c159656211ab1ab0717bd91c4c /Source/Dafny/Printer.cs | |
| parent | b4206512348cb4a3cdf87ccf7212e5193e8d3b35 (diff) | |
Support default (which, here, means nameless) class-instance constructors
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 7b5c1d42..e85c5e20 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -338,7 +338,8 @@ namespace Microsoft.Dafny { string k = method is Constructor ? "constructor" : "method";
if (method.IsStatic) { k = "static " + k; }
if (method.IsGhost) { k = "ghost " + k; }
- PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);
+ string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;
+ PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs);
if (method.SignatureIsOmitted) {
wr.WriteLine(" ...");
} else {
@@ -840,9 +841,14 @@ namespace Microsoft.Dafny { s = ", ";
}
wr.Write("]");
- } else if (t.InitCall != null) {
- wr.Write(".{0}(", t.InitCall.MethodName);
- PrintExpressionList(t.InitCall.Args);
+ } else if (t.Arguments == null) {
+ // nothing else to print
+ } else {
+ if (t.OptionalNameComponent != null) {
+ wr.Write(".{0}", t.OptionalNameComponent);
+ }
+ wr.Write("(");
+ PrintExpressionList(t.Arguments);
wr.Write(")");
}
} else {
|