Fixed latent crash of hovertext/outlining with include.

(This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.)

2 files changed, 103 insertions, 73 deletions

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index d638cb6c..51f837f7 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -77,7 +77,7 @@ namespace DafnyLanguage
       int start = entire.Start;

       int end = entire.End;

       foreach (var r in _regions) {

-        if (0 <= r.Length && r.Start >= start && r.Start + r.Length <= end) {

+        if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {

           DafnyTokenKind kind;

           switch (r.Kind) {

             case IdRegion.OccurrenceKind.Use:

@@ -136,7 +136,7 @@ namespace DafnyLanguage
       List<IdRegion> newRegions = new List<IdRegion>();

 

       foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) {

-        IdRegion.Add(newRegions, info.token, info.message, info.token.val.Length);

+        IdRegion.Add(newRegions, program, info.token, info.message, info.token.val.Length);

       }

 

       foreach (var module in program.Modules) {

@@ -149,29 +149,29 @@ namespace DafnyLanguage
             foreach (var ctor in dt.Ctors) {

               foreach (var dtor in ctor.Destructors) {

                 if (dtor.CorrespondingFormal.HasName) {

-                  IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module);

+                  IdRegion.Add(newRegions, program, dtor.tok, dtor, null, "destructor", true, module);

                 }

               }

             }

           } else if (d is IteratorDecl) {

             var iter = (IteratorDecl)d;

             foreach (var p in iter.Ins) {

-              IdRegion.Add(newRegions, p.tok, p, true, module);

+              IdRegion.Add(newRegions, program, p.tok, p, true, module);

             }

             foreach (var p in iter.Outs) {

-              IdRegion.Add(newRegions, p.tok, p, true, "yield-parameter", module);

+              IdRegion.Add(newRegions, program, p.tok, p, true, "yield-parameter", module);

             }

-            iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));

-            iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));

-            iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, module));

-            iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, module));

-            iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, module));

-            iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, module));

+            iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));

+            iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));

+            iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, program, module));

+            iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, program, module));

+            iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, program, module));

+            iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, program, module));

             if (!((ICallable)iter).InferredDecreases) {

-              iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));

+              iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));

             }

             if (iter.Body != null) {

-              StatementRegions(iter.Body, newRegions, module);

+              StatementRegions(iter.Body, newRegions, program, module);

             }

 

           } else if (d is ClassDecl) {

@@ -182,42 +182,42 @@ namespace DafnyLanguage
               } else  if (member is Function) {

                 var f = (Function)member;

                 foreach (var p in f.Formals) {

-                  IdRegion.Add(newRegions, p.tok, p, true, module);

+                  IdRegion.Add(newRegions, program, p.tok, p, true, module);

                 }

-                f.Req.ForEach(e => ExprRegions(e, newRegions, module));

-                f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));

-                f.Ens.ForEach(e => ExprRegions(e, newRegions, module));

-                f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));

+                f.Req.ForEach(e => ExprRegions(e, newRegions, program, module));

+                f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));

+                f.Ens.ForEach(e => ExprRegions(e, newRegions, program, module));

+                f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));

                 if (f.Body != null) {

-                  ExprRegions(f.Body, newRegions, module);

+                  ExprRegions(f.Body, newRegions, program, module);

                 }

               } else if (member is Method) {

                 var m = (Method)member;

                 foreach (var p in m.Ins) {

-                  IdRegion.Add(newRegions, p.tok, p, true, module);

+                  IdRegion.Add(newRegions, program, p.tok, p, true, module);

                 }

                 foreach (var p in m.Outs) {

-                  IdRegion.Add(newRegions, p.tok, p, true, module);

+                  IdRegion.Add(newRegions, program, p.tok, p, true, module);

                 }

-                m.Req.ForEach(e => ExprRegions(e.E, newRegions, module));

-                m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));

-                m.Ens.ForEach(e => ExprRegions(e.E, newRegions, module));

-                m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));

+                m.Req.ForEach(e => ExprRegions(e.E, newRegions, program, module));

+                m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));

+                m.Ens.ForEach(e => ExprRegions(e.E, newRegions, program, module));

+                m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));

                 if (m.Body != null) {

-                  StatementRegions(m.Body, newRegions, module);

+                  StatementRegions(m.Body, newRegions, program, module);

                 }

               } else if (member is SpecialField) {

                 // do nothing

               } else if (member is Field) {

                 var fld = (Field)member;

-                IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);

+                IdRegion.Add(newRegions, program, fld.tok, fld, null, "field", true, module);

               }

             }

           } else if (d is NewtypeDecl) {

             var dd = (NewtypeDecl)d;

             if (dd.Var != null) {

-              IdRegion.Add(newRegions, dd.Var.tok, dd.Var, true, module);

-              ExprRegions(dd.Constraint, newRegions, module);

+              IdRegion.Add(newRegions, program, dd.Var.tok, dd.Var, true, module);

+              ExprRegions(dd.Constraint, newRegions, program, module);

             }

           }

         }

@@ -228,54 +228,56 @@ namespace DafnyLanguage
       return true;

     }

 

-    static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, ModuleDefinition module) {

+    static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, Microsoft.Dafny.Program prog, ModuleDefinition module) {

       Contract.Requires(fe != null);

       Contract.Requires(regions != null);

+      Contract.Requires(prog != null);

       if (descendIntoExpressions) {

-        ExprRegions(fe.E, regions, module);

+        ExprRegions(fe.E, regions, prog, module);

       }

       if (fe.Field != null) {

         Microsoft.Dafny.Type showType = null;  // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression)

-        IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module);

+        IdRegion.Add(regions, prog, fe.tok, fe.Field, showType, "field", false, module);

       }

     }

 

-    static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {

+    static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, Microsoft.Dafny.Program prog, ModuleDefinition module) {

       Contract.Requires(expr != null);

       Contract.Requires(regions != null);

+      Contract.Requires(prog != null);

       if (expr is AutoGeneratedExpression) {

         // do nothing

         return;

       } else if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

-        IdRegion.Add(regions, e.tok, e.Var, false, module);

+        IdRegion.Add(regions, prog, e.tok, e.Var, false, module);

       } else if (expr is MemberSelectExpr) {

         var e = (MemberSelectExpr)expr;

         var field = e.Member as Field;

         if (field != null) {

-          IdRegion.Add(regions, e.tok, field, e.Type, "field", false, module);

+          IdRegion.Add(regions, prog, e.tok, field, e.Type, "field", false, module);

         }

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

         foreach (var bv in e.BoundVars) {

-          IdRegion.Add(regions, bv.tok, bv, true, module);

+          IdRegion.Add(regions, prog, bv.tok, bv, true, module);

         }

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         foreach (var bv in e.BoundVars) {

-          IdRegion.Add(regions, bv.tok, bv, true, module);

+          IdRegion.Add(regions, prog, bv.tok, bv, true, module);

         }

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

         foreach (var kase in e.Cases) {

           kase.Arguments.ForEach(bv => {

-            IdRegion.Add(regions, bv.tok, bv, true, module);

+            IdRegion.Add(regions, prog, bv.tok, bv, true, module);

             // if the arguments is an encapsulation of different boundvars from nested match cases,

             // add the boundvars so that they can show up in the IDE correctly

             if (bv.tok is MatchCaseToken) {

               MatchCaseToken mt = (MatchCaseToken)bv.tok;

               foreach(Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {

-                IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module);

+                IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module);

               }

             }

           });

@@ -283,22 +285,23 @@ namespace DafnyLanguage
       } else if (expr is ChainingExpression) {

         var e = (ChainingExpression)expr;

         // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression)

-        e.Operands.ForEach(ee => ExprRegions(ee, regions, module));

+        e.Operands.ForEach(ee => ExprRegions(ee, regions, prog, module));

         return;  // return here, so as to avoid doing the subexpressions below

       }

       foreach (var ee in expr.SubExpressions) {

-        ExprRegions(ee, regions, module);

+        ExprRegions(ee, regions, prog, module);

       }

     }

 

-    static void StatementRegions(Statement stmt, List<IdRegion> regions, ModuleDefinition module) {

+    static void StatementRegions(Statement stmt, List<IdRegion> regions, Microsoft.Dafny.Program prog, ModuleDefinition module) {

       Contract.Requires(stmt != null);

       Contract.Requires(regions != null);

+      Contract.Requires(prog != null);

       if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

         // Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's)

         foreach (var local in s.Locals) {

-          IdRegion.Add(regions, local.Tok, local, true, module);

+          IdRegion.Add(regions, prog, local.Tok, local, true, module);

         }

         if (s.Update == null) {

           // the VarDeclStmt has no associated assignment

@@ -306,29 +309,29 @@ namespace DafnyLanguage
           var upd = (UpdateStmt)s.Update;

           foreach (var rhs in upd.Rhss) {

             foreach (var ee in rhs.SubExpressions) {

-              ExprRegions(ee, regions, module);

+              ExprRegions(ee, regions, prog, module);

             }

           }

         } else {

           var upd = (AssignSuchThatStmt)s.Update;

-          ExprRegions(upd.Expr, regions, module);

+          ExprRegions(upd.Expr, regions, prog, module);

         }

         // we're done, so don't do the sub-statements/expressions again

         return;

       } else if (stmt is ForallStmt) {

         var s = (ForallStmt)stmt;

-        s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));

+        s.BoundVars.ForEach(bv => IdRegion.Add(regions, prog, bv.tok, bv, true, module));

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         foreach (var kase in s.Cases) {

           kase.Arguments.ForEach(bv => {

-            IdRegion.Add(regions, bv.tok, bv, true, module);

+            IdRegion.Add(regions, prog, bv.tok, bv, true, module);

             // if the arguments is an encapsulation of different boundvars from nested match cases,

             // add the boundvars so that they can show up in the IDE correctly

             if (bv.tok is MatchCaseToken) {

               MatchCaseToken mt = (MatchCaseToken)bv.tok;

               foreach (Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {

-                IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module);

+                IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module);

               }

             }              

           });

@@ -336,28 +339,28 @@ namespace DafnyLanguage
       } else if (stmt is LoopStmt) {

         var s = (LoopStmt)stmt;

         if (s.Mod.Expressions != null) {

-          s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module));

+          s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, prog, module));

         }

       } else if (stmt is CalcStmt) {

         var s = (CalcStmt)stmt;

         // skip the last line, which is just a duplicate anyway

         for (int i = 0; i < s.Lines.Count - 1; i++) {

-          ExprRegions(s.Lines[i], regions, module);

+          ExprRegions(s.Lines[i], regions, prog, module);

         }

         foreach (var ss in stmt.SubStatements) {

-          StatementRegions(ss, regions, module);

+          StatementRegions(ss, regions, prog, module);

         }

         return;

       }

       foreach (var ee in stmt.SubExpressions) {

-        ExprRegions(ee, regions, module);

+        ExprRegions(ee, regions, prog, module);

       }

       foreach (var ss in stmt.SubStatements) {

-        StatementRegions(ss, regions, module);

+        StatementRegions(ss, regions, prog, module);

       }

     }

 

-    class IdRegion

+    class IdRegion : DafnyRegion

     {

       public readonly int Start;

       public readonly int Length;

@@ -366,31 +369,41 @@ namespace DafnyLanguage
       public readonly OccurrenceKind Kind;

       public readonly IVariable Variable;

 

-      public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {

+      public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(regions != null);

+        Contract.Requires(prog != null);

         Contract.Requires(tok != null);

         Contract.Requires(v != null);

-        Add(regions, tok, v, isDefinition, null, context);

+        Add(regions, prog, tok, v, isDefinition, null, context);

       }

-      public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {

+      public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {

         Contract.Requires(regions != null);

+        Contract.Requires(prog != null);

         Contract.Requires(tok != null);

         Contract.Requires(v != null);

-        regions.Add(new IdRegion(tok, v, isDefinition, kind, context));

+        if (InMainFile(prog, tok)) {

+          regions.Add(new IdRegion(tok, v, isDefinition, kind, context));

+        }

       }

-      public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {

+      public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(regions != null);

+        Contract.Requires(prog != null);

         Contract.Requires(tok != null);

         Contract.Requires(decl != null);

         Contract.Requires(kind != null);

-        regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));

+        if (InMainFile(prog, tok)) {

+          regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));

+        }

       }

 

-      public static void Add(List<IdRegion> regions, Bpl.IToken tok, string text, int length) {

+      public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, string text, int length) {

         Contract.Requires(regions != null);

+        Contract.Requires(prog != null);

         Contract.Requires(tok != null);

         Contract.Requires(text != null);

-        regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));

+        if (InMainFile(prog, tok)) {

+          regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));

+        }

       }

 

       private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {

@@ -442,6 +455,15 @@ namespace DafnyLanguage
     }

   }

 

+  public abstract class DafnyRegion

+  {

+    public static bool InMainFile(Microsoft.Dafny.Program prog, Bpl.IToken tok) {

+      Contract.Requires(prog != null);

+      Contract.Requires(tok != null);

+      return object.Equals(prog.FullName, tok.filename);

+    }

+  }

+

   #endregion

 

 }

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index 85771e94..ea611594 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -80,7 +80,7 @@ namespace DafnyLanguage
       if (start == end) yield break;

 

       foreach (var r in _regions) {

-        if (0 <= r.Length && r.Start >= start && r.Start + r.Length <= end) {

+        if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {

           yield return new TagSpan<OutliningRegionTag>(

             new SnapshotSpan(_snapshot, r.Start, r.Length),

             new OutliningRegionTag(false, false, "...", r.HoverText));

@@ -130,18 +130,18 @@ namespace DafnyLanguage
           if (module.IsAbstract) {

             nm = "abstract " + nm;

           }

-          newRegions.Add(new OutliningRegion(module, nm));

+          OutliningRegion.Add(newRegions, program, module, nm);

         }

         foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {

           if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {

             continue;

           }

           if (d is Dafny.OpaqueTypeDecl) {

-            newRegions.Add(new OutliningRegion(d, "type"));

+            OutliningRegion.Add(newRegions, program, d, "type");

           } else if (d is Dafny.CoDatatypeDecl) {

-            newRegions.Add(new OutliningRegion(d, "codatatype"));

+            OutliningRegion.Add(newRegions, program, d, "codatatype");

           } else if (d is Dafny.DatatypeDecl) {

-            newRegions.Add(new OutliningRegion(d, "datatype"));

+            OutliningRegion.Add(newRegions, program, d, "datatype");

           } else if (d is Dafny.ModuleDecl) {

             // do nothing here, since the outer loop handles modules

           } else {

@@ -149,9 +149,9 @@ namespace DafnyLanguage
             if (cl.IsDefaultClass) {

               // do nothing

             } else if (cl is Dafny.IteratorDecl) {

-              newRegions.Add(new OutliningRegion(cl, "iterator"));

+              OutliningRegion.Add(newRegions, program, cl, "iterator");

             } else {

-              newRegions.Add(new OutliningRegion(cl, "class"));

+              OutliningRegion.Add(newRegions, program, cl, "class");

             }

             // do the class members (in particular, functions and methods)

             foreach (Dafny.MemberDecl m in cl.Members) {

@@ -168,7 +168,7 @@ namespace DafnyLanguage
                 if (!m.IsGhost) {

                   nm += " method";

                 }

-                newRegions.Add(new OutliningRegion(m, nm));

+                OutliningRegion.Add(newRegions, program, m, nm);

               } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {

                 var nm =

                   m is Dafny.Constructor ? "constructor" :

@@ -179,7 +179,7 @@ namespace DafnyLanguage
                 if (m.IsGhost && !(m is Dafny.CoLemma)) {

                   nm = "ghost " + nm;

                 }

-                newRegions.Add(new OutliningRegion(m, nm));

+                OutliningRegion.Add(newRegions, program, m, nm);

               }

             }

           }

@@ -196,12 +196,20 @@ namespace DafnyLanguage
       return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;

     }

 

-    class OutliningRegion

+    class OutliningRegion : DafnyRegion

     {

+      public static void Add(List<OutliningRegion> regions, Microsoft.Dafny.Program prog, Dafny.INamedRegion decl, string kind) {

+        Contract.Requires(regions != null);

+        Contract.Requires(prog != null);

+        if (InMainFile(prog, decl.BodyStartTok)) {

+          regions.Add(new OutliningRegion(decl, kind));

+        }

+      }

+

       public readonly int Start;

       public readonly int Length;

       public readonly string HoverText;

-      public OutliningRegion(Dafny.INamedRegion decl, string kind) {

+      private OutliningRegion(Dafny.INamedRegion decl, string kind) {

         int startPosition = decl.BodyStartTok.pos + 1;  // skip the open-curly brace itself

         int length = decl.BodyEndTok.pos - startPosition;

         Start = startPosition;