Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

option to supress variables bound to _, in info view #100

Closed
ratmice opened this issue Dec 7, 2018 · 3 comments
Closed

option to supress variables bound to _, in info view #100

ratmice opened this issue Dec 7, 2018 · 3 comments

Comments

@ratmice
Copy link
Contributor

ratmice commented Dec 7, 2018

When binding like: (\lam a _, a), in the info view, it will list a variable e.g. _x : ...
It would perhaps be a nice enhancement if it were possible show/hide these bindings beginning with _ in the info view.
@PatrickMassot
Copy link
Contributor

I already suggested this in order to hide instances. It would be really nice to have a filtering toggle button next to the updating toggle.

@bryangingechen bryangingechen mentioned this issue Dec 27, 2018
Merged
@bryangingechen
Copy link
Contributor

I've just made PR #101 which is an attempt in this direction. Please test it out and leave comments there!

@bryangingechen bryangingechen mentioned this issue Dec 28, 2018
Merged
@gebner gebner mentioned this issue Jan 8, 2019
Open
@ratmice
Copy link
Contributor Author

ratmice commented Jan 11, 2019

With Bryan's PR merged, i think this can be closed.

@ratmice ratmice closed this as completed Jan 11, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ratmice @bryangingechen @PatrickMassot