Members included from different files are now internally marked with an IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features.

Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines).
Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked.

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index b608a6e2..f604ebe6 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -86,13 +86,13 @@ namespace Microsoft.Dafny {
     // Lower-case file names before comparing them, since Windows uses case-insensitive file names

     private class IncludeComparer : IComparer<Include> {

       public int Compare(Include x, Include y) {

-        return x.filename.ToLower().CompareTo(y.filename.ToLower());

+        return x.fullPath.ToLower().CompareTo(y.fullPath.ToLower());

       }

     }

 

     public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, Errors errs) {

       SortedSet<Include> includes = new SortedSet<Include>(new IncludeComparer());

-      bool newlyIncluded = false;

+      bool newlyIncluded;

       do {

         newlyIncluded = false;