Skip to content

Commit 5d05800

Browse files
authored
chore: set hasWidgets configuration option
See leanprover/lean4#981 .
1 parent a243e5a commit 5d05800

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

vscode-lean4/src/leanclient.ts

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,7 @@ export class LeanClient implements Disposable {
132132
documentSelector: [documentSelector],
133133
initializationOptions: {
134134
editDelay: getElaborationDelay(),
135+
hasWidgets: true,
135136
},
136137
middleware: {
137138
handleDiagnostics: (uri, diagnostics, next) => {

0 commit comments

Comments
 (0)