search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

Improve automatic proof search by supporting options #50

Closed andrevidela closed 7 years ago

andrevidela commented 7 years ago

When using emacs it is possible to change the behaviour of c-c c-a to get more information about the search.

This document lists all the options that can be put inside a hole to modify the behaviour of c-c c-a https://github.com/agda/agda/blob/master/doc/user-manual/tools/auto.rst

It would be nice if agda-mode supported those options as well.

banacorn commented 7 years ago

Thanks a lot!

I simply changed a line of code from this:

core.view.set('Auto', ['No solution found'], View.Style.Info);

to this:

core.view.set('Auto', response.content, View.Style.Info);

voilà!

It turned out that I have been ignoring Agda ever since.