Right-clicking on a state allows to display the source code for it

1 files changed, 6 insertions, 3 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index bcad3ca5..0a032f06 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -30,7 +30,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

   class DafnyModel : LanguageModel

   {

-    public readonly Model model;

     public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field, f_dtype, f_null;

     public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();

     public readonly Dictionary<Model.Element, Model.FuncTuple> DatatypeValues = new Dictionary<Model.Element, Model.FuncTuple>();

@@ -38,9 +37,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     public List<StateNode> states = new List<StateNode>();

 

     public DafnyModel(Model m, ViewOptions opts)

-      : base(opts)

+      : base(m, opts)

     {

-      model = m;

       f_heap_select = m.MkFunc("[3]", 3);

       f_set_select = m.MkFunc("[2]", 2);

       f_seq_length = m.MkFunc("Seq#Length", 1);

@@ -327,6 +325,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       }

     }

 

+    public SourceLocation ShowSource()

+    {

+      return dm.GetSourceLocation(state);

+    }

+

   }

 

   class ElementNode : DisplayNode