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

Save REPL history to file .dotty_history in home directory #5252

Merged
merged 1 commit into from Oct 17, 2018

Conversation

Projects
None yet
5 participants
@nrjais
Copy link
Contributor

nrjais commented Oct 13, 2018

Fixes #5142

@dotty-bot
Copy link

dotty-bot left a comment

Hello, and thank you for opening this PR! 🎉

All contributors have signed the CLA, thank you! ❤️

Have an awesome day! ☀️

@allanrenucci
Copy link
Member

allanrenucci left a comment

LGTM. Thanks @nrjais

@allanrenucci allanrenucci merged commit 3c196b5 into lampepfl:master Oct 17, 2018

2 checks passed

CLA User signed CLA
Details
continuous-integration/drone/pr the build was successful
Details
.terminal(terminal)
.history(history)
.completer(completer)
.highlighter(new Highlighter)
.parser(new Parser)
.variable(HISTORY_FILE, s"$userHome/.dotty_history") // Save history to file

This comment has been minimized.

@smarter

smarter Oct 17, 2018

Member

Does this work on Windows or do we need File.pathSeparator instead of / here too ?

This comment has been minimized.

@allanrenucci

allanrenucci Oct 17, 2018

Member

This goes through java.nio.file.Paths. I believe it handles path separator correctly

This comment has been minimized.

@smarter

smarter Oct 17, 2018

Member

Ok. Note for later: To be perfect we probably shouldn't write files directly in the home directory, on Linux you should use $HOME/.config/nameofyourapplication/ and on Windows there's some other folder, but this is hard to handle correctly. There's https://github.com/soc/directories-jvm that is designed to do that for you, but it doesn't seem to have a stable ABI so we'd have to embed it in our sources.

This comment has been minimized.

@milessabin

milessabin Oct 18, 2018

Contributor

I think $HOME/.dotty_history is the right place on Linux. A history file isn't a configuration file, so it doesn't belong under $HOME/.config. Also cp. $HOME/.scala_history, $HOME/.histfile, $HOME/.bash_history and many, many more ...

For configuration files on Linux, if you're going to bother with the XDG spec, you should first check if $XDG_CONFIG_HOME is set and only default to $HOME/.config if it isn't. But bear in mind that standards schmandards and lots of configuration stuff still quite happily lives in dotfiles directly in $HOME.

@nrjais nrjais deleted the nrjais:repl-history branch Oct 17, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment