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

Reload Arend libraries misplaced. #501

Closed
sxhya opened this issue May 21, 2024 · 0 comments
Closed

Reload Arend libraries misplaced. #501

sxhya opened this issue May 21, 2024 · 0 comments
Assignees
@alex999990009
Labels
gui

Comments

@sxhya
Copy link
Collaborator

sxhya commented May 21, 2024 •
edited
Loading

  1. Reload Arend Libraries feature is currently available in the popup menu for individual Arend files (in the Project pane). It should not be there as it has global effect (does not depend on the item chosen in Popup)
  2. Instead, a separate Arend Actions menu should be created in the Tools menu and the Reload Arend Libraries feature should be moved there.
  3. Existing Show Arend REPL feature (in Tools Menu) should also be moved into Arend Actions menu
  4. Arend Actions Menu should have our pink A logo on it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@alex999990009 alex999990009

Labels
gui
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@sxhya @alex999990009