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

Document features (and add fancy gifs) #9

Merged
merged 9 commits into from
Dec 12, 2024
Merged

Document features (and add fancy gifs) #9

merged 9 commits into from
Dec 12, 2024

Conversation

xvw
Copy link
Member

@xvw xvw commented Dec 10, 2024

No description provided.

@xvw xvw requested a review from voodoos December 10, 2024 14:04
Copy link
Member

@voodoos voodoos left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

First round of commands, this looks great overall !

from an expression to the parent `let`, the parent `module`, the
parent `fun` and the parent `match` expression. It is also possible to
navigate between pattern matching cases:

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should indicate the targets for pattern matching cases. Even better, could they appear as suggestions when calling the command ?

The custom request can also return all possible targets with the corresponding jump, that might be a better workflow ?

  • Execute the command which wait for the CR answer
  • Ask the user which of the available jumps she wants to perform.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh yes, non giving a target will compute every available targets?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes !

@xvw xvw merged commit 6e95199 into main Dec 12, 2024
4 checks passed
@xvw xvw deleted the media-on-README branch December 12, 2024 15:31
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

Successfully merging this pull request may close these issues.

2 participants