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.

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

Add new commands to repl :show import (to show already imported modules) and :show loaded (all available) #3410

Open
2 tasks
srghma opened this issue Nov 2, 2024 · 0 comments

Comments

@srghma
Copy link

srghma commented Nov 2, 2024

  • I have read CONTRIBUTING.md.
  • I have checked that there is no existing PR/issue about my proposal.

Motivation

will be used in idris-community/idris2-lsp#227

Examples

so, if I have dependencies = base, filepath in ipkg, then :show loaded will show Data.Vect and Data.FilePath and Data.FilePath.File, etc.

just like in purescript

2024-11-02-02pm-48-12-screenshot

Technical implementation

Alternatives considered

maybe better

  1. show imported_modules - modules in scope, e.g. import Data.Vect (same as show import from purescript)
  2. show loaded_modules - all available modules from all available packages ( same as show loaded from purescript)
  3. show imported_packages - IF before I did :package "filepath" THEN will show filepath - imported completely ELSEIF before I did import Data.Vect THEN will show base - imported partially
  4. show loaded_packages - if dependencies = base, filepath then will show base, filepath

Conclusion

@srghma srghma changed the title Add new command to repl :get_available_imports Add new command to repl :show loaded Nov 2, 2024
@srghma srghma changed the title Add new command to repl :show loaded Add new commands to repl :show import (to show already imported modules) and :show loaded (all available) Nov 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant