search

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

Reload Arend libraries misplaced. #501

Closed sxhya closed 5 months ago

sxhya commented 5 months ago
  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.