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鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

stage2: make repl ui better #8500

Closed
wants to merge 1 commit into from
Closed

stage2: make repl ui better #8500

wants to merge 1 commit into from

Conversation

g-w1
Copy link
Contributor

@g-w1 g-w1 commented Apr 12, 2021

As stage2 is improving, I found myself using this repl more and more and it was annoying to type out update every time, so I updated the ui.
"" runs the previous command
Any first letter for a command also works for the command itself. As we add more commands, this could be fleshed out more to avoid collisions.
I made it print updating... every time so that if you did "" and it took a short time 馃コ you would know it was actually updating and not just skipping. Should a different message print here?

@andrewrk
Copy link
Member

I made it print updating... every time so that if you did "" and it took a short time partying_face you would know it was actually updating and not just skipping. Should a different message print here?

It should print nothing because we already have the progress bar that shows up after 0.5 seconds!

However if we want to indicate that an update occurred, we could have it print something more useful such as:

Update completed; 3/100 files changed, 123/900 decls modified, 12 added, 34 deleted

or something to that effect.

@g-w1
Copy link
Contributor Author

g-w1 commented Apr 12, 2021

Thanks, this is just the kind of feedback I was looking for!

@g-w1
Copy link
Contributor Author

g-w1 commented Apr 12, 2021

I found finding added/deleted decls hard, but I think this is good enough for now:
image

This adds an indicator of how many decls were updated.
It also allows you to use the first letter of command instead
of it and "" to execute the previous command.
@g-w1
Copy link
Contributor Author

g-w1 commented Apr 21, 2021

Ok, finally got around to making it show how many were added or removed thanks to help from andrewrk on irc.

@g-w1
Copy link
Contributor Author

g-w1 commented May 19, 2021

I will rebase soon as #8554 was merged and included a lot of the same kinds of stuff.

@g-w1
Copy link
Contributor Author

g-w1 commented May 22, 2021

Closing as actually the features that I most wanted were added.

@g-w1 g-w1 closed this May 22, 2021
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.

None yet

2 participants