Skip to content

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

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.

Sign up for GitHub

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

Merged
merged 1 commit into from
Oct 17, 2018
Merged

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/repl/JLineTerminal.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,12 +47,15 @@ final class JLineTerminal(needsTerminal: Boolean) extends java.io.Closeable {
)(implicit ctx: Context): String = {
import LineReader.Option._
import LineReader._
val lineReader = LineReaderBuilder.builder()
val userHome = System.getProperty("user.home")
val lineReader = LineReaderBuilder
.builder()
.terminal(terminal)
.history(history)
.completer(completer)
.highlighter(new Highlighter)
.parser(new Parser)
.variable(HISTORY_FILE, s"$userHome/.dotty_history") // Save history to file
Copy link
Member

Choose a reason for hiding this comment

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

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

Copy link
Contributor

Choose a reason for hiding this comment

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

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

Copy link
Member

Choose a reason for hiding this comment

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

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.

Copy link
Contributor

Choose a reason for hiding this comment

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

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.

.variable(SECONDARY_PROMPT_PATTERN, "%M") // A short word explaining what is "missing",
// this is supplied from the EOFError.getMissing() method
.variable(LIST_MAX, 400) // Ask user when number of completions exceed this limit (default is 100).
Expand Down