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.cs31
1 files changed, 14 insertions, 17 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 5c5c95b5..1e2424ed 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -53,17 +53,6 @@ namespace Microsoft.Dafny {
} else if (d is DatatypeDecl) {
if (i++ != 0) { wr.WriteLine(); }
PrintDatatype((DatatypeDecl)d, indent);
- } else if (d is ClassDecl) {
- ClassDecl cl = (ClassDecl)d;
- if (!cl.IsDefaultClass) {
- if (i++ != 0) { wr.WriteLine(); }
- PrintClass(cl, indent);
- } else if (cl.Members.Count == 0) {
- // print nothing
- } else {
- if (i++ != 0) { wr.WriteLine(); }
- PrintMembers(cl.Members, indent);
- }
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
Indent(indent);
@@ -106,19 +95,27 @@ namespace Microsoft.Dafny {
if (DafnyOptions.O.DafnyPrintResolvedFile != null) {
// also print the members that were created as part of the interpretation of the iterator
- Contract.Assert(iter.ImplicitlyDefinedMembers != null); // filled in during resolution
- var members = new List<MemberDecl>();
- foreach (var m in iter.ImplicitlyDefinedMembers.Values) {
- members.Add(m);
- }
+ Contract.Assert(iter.Members.Count != 0); // filled in during resolution
wr.WriteLine("/*---------- iterator members ----------");
PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);
wr.WriteLine(" {");
- PrintMembers(members, indent + IndentAmount);
+ PrintMembers(iter.Members, indent + IndentAmount);
Indent(indent); wr.WriteLine("}");
wr.WriteLine("---------- iterator members ----------*/");
}
+ } else if (d is ClassDecl) {
+ ClassDecl cl = (ClassDecl)d;
+ if (!cl.IsDefaultClass) {
+ if (i++ != 0) { wr.WriteLine(); }
+ PrintClass(cl, indent);
+ } else if (cl.Members.Count == 0) {
+ // print nothing
+ } else {
+ if (i++ != 0) { wr.WriteLine(); }
+ PrintMembers(cl.Members, indent);
+ }
+
} else if (d is ModuleDecl) {
wr.WriteLine();
Indent(indent);