Allow the provider to skip some states when generating SourceLocations

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 50783c44..721ee182 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         var sn = new StateNode(dm.states.Count, dm, s);

         dm.states.Add(sn);

       }

+      dm.FinishStates();

       return dm;

     }

   }

@@ -77,6 +78,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       }

     }

 

+    internal void FinishStates()

+    {

+      GenerateSourceLocations(states);

+    }

+

     public override IEnumerable<IState> States

     {

       get { return states; }