File tree Expand file tree Collapse file tree 1 file changed +27
-0
lines changed Expand file tree Collapse file tree 1 file changed +27
-0
lines changed Original file line number Diff line number Diff line change 287
287
}
288
288
],
289
289
"menus" : {
290
+ "editor/context" : [
291
+ {
292
+ "when" : " resourceLangId == coq" ,
293
+ "command" : " extension.coq.interpretToPoint" ,
294
+ "group" : " navigation"
295
+ },
296
+ {
297
+ "when" : " resourceLangId == coq" ,
298
+ "command" : " extension.coq.query.check" ,
299
+ "group" : " queries"
300
+ },
301
+ {
302
+ "when" : " resourceLangId == coq" ,
303
+ "command" : " extension.coq.query.print" ,
304
+ "group" : " queries"
305
+ },
306
+ {
307
+ "when" : " resourceLangId == coq" ,
308
+ "command" : " extension.coq.query.search" ,
309
+ "group" : " queries"
310
+ },
311
+ {
312
+ "when" : " resourceLangId == coq" ,
313
+ "command" : " extension.coq.query.locate" ,
314
+ "group" : " queries"
315
+ }
316
+ ],
290
317
"view/title" : [
291
318
{
292
319
"command" : " extension.coq.addQueryTab" ,
You can’t perform that action at this time.
0 commit comments