Save REPL history to file .dotty_history in home directory #5252
Conversation
| .terminal(terminal) | ||
| .history(history) | ||
| .completer(completer) | ||
| .highlighter(new Highlighter) | ||
| .parser(new Parser) | ||
| .variable(HISTORY_FILE, s"$userHome/.dotty_history") // Save history to file |
There was a problem hiding this comment.
Does this work on Windows or do we need File.pathSeparator instead of / here too ?
There was a problem hiding this comment.
This goes through java.nio.file.Paths. I believe it handles path separator correctly
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
Fixes #5142