markokoleznik / agda-writer

A simple GUI for Agda
Other
31 stars 2 forks source link

Highlight goal when inside it. #24

Closed andrejbauer closed 9 years ago

andrejbauer commented 9 years ago

It would be nice to hhighlight the goal in the upper-right when the cursor is inside the corresponding {! ... !}. Also, I tend to use spaces, so {! blah !} instead of {!blah!}, but I do not know if there is an adopted standard.