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

:browse seems wrong when given parameters #689

Open
yav opened this issue Mar 24, 2020 · 4 comments
Open

:browse seems wrong when given parameters #689

yav opened this issue Mar 24, 2020 · 4 comments
Labels
command-line-repl Related to Cryptol's text-based UI feature request Asking for new or improved functionality parameterized modules Related to Cryptol's parameterized modules

Comments

@yav
Copy link
Member

yav commented Mar 24, 2020

The current behavior of :browse M is to see information about names defined in M from the point of view of the currently focused module. This means that you only ever get to see information about public names in M and only if you imported them.

This seems confusing. I propose that we change :browse to work as follows:

  1. :browse with no parameters shows information about what's current in scope at the REPL. This includes the currently focused module, plus any dynamic bindings (e.g., let bound, or it)
  2. :browse M shows all information about M, no matter what's currently in scope at the REPL.

Thoughts?

@yav yav added command-line-repl Related to Cryptol's text-based UI feature request Asking for new or improved functionality labels Mar 24, 2020
@brianhuffman
Copy link
Contributor

Just to be clear: You're not proposing that :browse show information about arbitrary modules, only modules that are currently loaded; is that right? If so, then I think your proposal is totally reasonable. I didn't put much thought into the behavior of the current :browse <module> command.

@yav
Copy link
Member Author

yav commented Mar 24, 2020

Oh yes, :browse is supposed to be read-only, so it will only work on already loaded modules.

yav added a commit that referenced this issue Mar 24, 2020
This implements the feature request in #689
yav added a commit that referenced this issue Mar 25, 2020
This implements the feature request in #689
@robdockins robdockins added the parameterized modules Related to Cryptol's parameterized modules label Mar 26, 2021
yav added a commit that referenced this issue Apr 2, 2021
This fixes a bug where the scoping on the command line was incorrect
for nested modules.

It also changes the semantics of `:browse` (whose implementation is now
in a separate module), to be more reasonable. See #689
@yav
Copy link
Member Author

yav commented Apr 2, 2021

I've just redone how browse works in the "Nested Modules" PR. I settled on the following semantics:

  1. :browse with no argument shows what's in scope at the command line
  2. :browse M shows what's exported by M (no matter what's in scope at the command line)

This seems simple an consistent, and is more or less what I'd want most of the time, I think.
Also, the way the code is written, it'd be fairly easy to show what's in scope in another module, but if we deem this useful, we could use a different command

@glguy
Copy link
Member

glguy commented Jul 9, 2024

PR #1682 introduces :focus that can be used to change the point-of-view into a submodule. From this state you can :browse to see the internal view of a submodule.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
command-line-repl Related to Cryptol's text-based UI feature request Asking for new or improved functionality parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

No branches or pull requests

4 participants