You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi there,
when completing a hypothesis name and scrolling in the completion popup menu, it would be nice to have the selected hypothesis be highlighted in the goals buffer. So that we can see its type.
Ideally the other names of the popup would also be highlighted but less visibly.
Note sure if I am able to propose a PR for that though.
Best
The text was updated successfully, but these errors were encountered:
Hi there,
when completing a hypothesis name and scrolling in the completion popup menu, it would be nice to have the selected hypothesis be highlighted in the goals buffer. So that we can see its type.
Ideally the other names of the popup would also be highlighted but less visibly.
Note sure if I am able to propose a PR for that though.
Best
The text was updated successfully, but these errors were encountered: