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

Structure panel should omit "let () = ..." items and should include "let (a,b) = ..." items #153

Closed
jfehrle opened this issue Mar 23, 2019 · 4 comments

Comments

@jfehrle
Copy link
Collaborator

jfehrle commented Mar 23, 2019

plugin version: 0.73

  1. Top level lets in the form let () = ... should not appear in the structure panel since they don't have name. For example:

image

  1. Top level lets in the form let (a, b) = ... should appear in the structure panel with names a and b. For example:

image

Code for the examples is here: https://github.com/coq/coq/blob/master/vernac/vernacentries.ml

@giraud
Copy link
Owner

giraud commented Mar 25, 2019

Fixed in 0.74

@giraud giraud closed this as completed Mar 25, 2019
@jfehrle
Copy link
Collaborator Author

jfehrle commented Mar 25, 2019

Looks better on # 1, thanks.

I would have split let (f_interp_redexp, interp_redexp_hook) into 2 separate entries in the structure panel. Both are top-level variables. They just happen to both be defined in the same let. If I'm looking for f_interp_redexp when the structure panel is alphabetized I'd expect to find it between focus_cmd_cond and get_current_context_of_args

image

Also, a different issue: I'd expect the opens to be alphabetized when the panel has alphabetic order selected. And probably I'd intermix them with other symbols.

image

@giraud
Copy link
Owner

giraud commented Apr 11, 2019

Fixed in 0.75

@giraud giraud closed this as completed Apr 11, 2019
@jfehrle
Copy link
Collaborator Author

jfehrle commented Apr 11, 2019

Looks good!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants