1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using Microsoft.VisualStudio.Text.Editor;
namespace DafnyLanguage
{
class MenuProxy : DafnyLanguage.DafnyMenu.IMenuProxy
{
private DafnyMenu.DafnyMenuPackage DafnyMenuPackage;
public MenuProxy(DafnyMenu.DafnyMenuPackage DafnyMenuPackage)
{
this.DafnyMenuPackage = DafnyMenuPackage;
}
public int ToggleSnapshotVerification(IWpfTextView activeTextView)
{
return DafnyDriver.ChangeIncrementalVerification(1);
}
public int ToggleMoreAdvancedSnapshotVerification(IWpfTextView activeTextView)
{
return DafnyDriver.ChangeIncrementalVerification(2);
}
public bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView)
{
return activeTextView != null
&& 0 < DafnyDriver.IncrementalVerificationMode();
}
public bool ToggleAutomaticInduction(IWpfTextView activeTextView) {
return DafnyDriver.ChangeAutomaticInduction();
}
public bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView) {
return activeTextView != null;
}
public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
return activeTextView != null
&& DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)
&& tagger != null && tagger.VerificationDisabled;
}
public void StopVerifier(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
{
tagger.StopVerification();
}
}
public bool RunVerifierCommandEnabled(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
return activeTextView != null
&& DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)
&& tagger != null && tagger.VerificationDisabled;
}
public void RunVerifier(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
{
tagger.StartVerification();
}
}
public void DiagnoseTimeouts(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
{
tagger.StartVerification(false, true);
}
}
public bool MenuEnabled(IWpfTextView activeTextView)
{
return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";
}
public bool CompileCommandEnabled(IWpfTextView activeTextView)
{
ResolverTagger resolver;
return activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null;
}
public bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView)
{
ResolverTagger resolver;
return activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.VerificationErrors.Any(err => err.Message.Contains("timed out"));
}
public void Compile(IWpfTextView activeTextView)
{
ResolverTagger resolver;
if (activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null)
{
var outputWriter = new StringWriter();
DafnyMenuPackage.ExecuteAsCompiling(() => { DafnyDriver.Compile(resolver.Program, outputWriter); }, outputWriter);
}
}
public bool ShowErrorModelCommandEnabled(IWpfTextView activeTextView)
{
ResolverTagger resolver;
return activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null
&& resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.ModelText));
}
public void ShowErrorModel(IWpfTextView activeTextView)
{
ResolverTagger resolver = null;
var show = activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null
&& resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
if (show)
{
var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
if (selectedError != null)
{
DafnyMenuPackage.ShowErrorModelInBVD(selectedError.ModelText, selectedError.SelectedStateId);
}
}
}
}
}
|
