DafnyExtension: Update the error model when a new error state is selected.

1 files changed, 4 insertions, 0 deletions

diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index acb8ccb0..e9f65b81 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -190,6 +190,10 @@ namespace DafnyLanguage
           esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;

           esrtag.Error.SelectedStateAdornment.ToolTip = "unselect state";

           esrtag.Error.SelectedStateId = esrtag.Id;

+          if (!string.IsNullOrEmpty(esrtag.Error.Model))

+          {

+            DafnyClassifier.DafnyMenuPackage.ShowErrorModel(esrtag.Error.Model, esrtag.Id);

+          }

         }

       });

       return result;