More line ending fixups.

3 files changed, 15 insertions, 15 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index cd026393..a0d0e583 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -120,7 +120,7 @@ void ObjectInvariant()
         } else if (m is CouplingInvariant) {

           wr.WriteLine();

           PrintCouplingInvariant((CouplingInvariant)m, indent);

-          state = 2;
+          state = 2;

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

         }

@@ -215,7 +215,7 @@ void ObjectInvariant()
       }

       wr.Write(" by ");

       PrintExpression(inv.Expr);

-      wr.WriteLine(";");
+      wr.WriteLine(";");

     }

     

     public void PrintFunction(Function f, int indent) {

@@ -287,7 +287,7 @@ void ObjectInvariant()
       }

       wr.WriteLine(method.Body == null ? ";" : "");

 

-      int ind = indent + IndentAmount;
+      int ind = indent + IndentAmount;

       PrintSpec("requires", method.Req, ind);

       PrintFrameSpecLine("modifies", method.Mod, ind);

       PrintSpec("ensures", method.Ens, ind);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 64a23393..ff658378 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -64,7 +64,7 @@ void ObjectInvariant()
     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       // register modules

-      Dictionary<string,ModuleDecl> modules = new Dictionary<string,ModuleDecl>();
+      Dictionary<string,ModuleDecl> modules = new Dictionary<string,ModuleDecl>();

       foreach (ModuleDecl m in prog.Modules) {

         if (modules.ContainsKey(m.Name)) {

           Error(m, "Duplicate module name: {0}", m.Name);

@@ -116,12 +116,12 @@ void ObjectInvariant()
         foreach (TopLevelDecl decl in m.TopLevelDecls) 

           if (decl is ClassRefinementDecl) {

             ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;

-            ResolveTopLevelRefinement(rdecl);
+            ResolveTopLevelRefinement(rdecl);

             if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

           }

       

       // attempt finding refinement cycles

-      List<TopLevelDecl> refinesCycle = refines.TryFindCycle();
+      List<TopLevelDecl> refinesCycle = refines.TryFindCycle();

       if (refinesCycle != null) {

         string cy = "";

         string sep = "";

@@ -293,7 +293,7 @@ void ObjectInvariant()
         } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

           if (currentClass is ClassRefinementDecl) {      

-            ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
+            ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

             if (refined != null) {

               Contract.Assert( classMembers.ContainsKey(refined));

               Dictionary<string,MemberDecl> members = classMembers[refined];

@@ -302,13 +302,13 @@ void ObjectInvariant()
               List<Field> fields = new List<Field>();

               foreach (IToken tok in inv.Toks) {

                 if (!members.ContainsKey(tok.val))

-                  Error(tok, "Refined class does not declare a field: {0}", tok.val);
+                  Error(tok, "Refined class does not declare a field: {0}", tok.val);

                 else {

                   MemberDecl field = members[tok.val];

                   if (!(field is Field)) 

                     Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

                   else if (fields.Contains(cce.NonNull((Field)field)))

-                    Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
+                    Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);

                   else

                     fields.Add(cce.NonNull((Field)field));

                 }                  

@@ -324,9 +324,9 @@ void ObjectInvariant()
         }

         

         if (currentClass is ClassRefinementDecl) {          

-          ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
+          ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

           if (refined != null) {

-            Contract.Assert( classMembers.ContainsKey(refined));
+            Contract.Assert( classMembers.ContainsKey(refined));

           

             // there is a member with the same name in refined class if and only if the member is a refined method

             if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

@@ -379,7 +379,7 @@ void ObjectInvariant()
                   if (mf.Ins.Count != mf.Refined.Ins.Count)

                     Error(mf, "Different number of input variables");

                   if (mf.Outs.Count != mf.Refined.Outs.Count)

-                    Error(mf, "Different number of output variables");
+                    Error(mf, "Different number of output variables");

                   if (mf.IsStatic || mf.Refined.IsStatic) 

                     Error(mf, "Refined methods cannot be static");

                 } else {

@@ -387,7 +387,7 @@ void ObjectInvariant()
                 }            

               }

             } else {

-              Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);
+              Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);

             }

           }

         

@@ -1783,7 +1783,7 @@ void ObjectInvariant()
           ResolveExpression(ee, twoState, specContext);

           Contract.Assert( ee.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(elementType, ee.Type)) {

-            Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
+            Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);

           }

         }

         if (expr is SetDisplayExpr) {

diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index c7be5420..66541236 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -35,7 +35,7 @@ void ObjectInvariant()
       }

       public void AddSuccessor(Vertex v) {

         Contract.Requires(v != null);

-        Successors.Add(v);
+        Successors.Add(v);

       }

     }