REPL doesn't work on Windows: Consider directly using JLine 3 for the REPL

[smarter]

The REPL UI code in Dotty comes from ammonite-terminal and lives in https://github.com/lampepfl/dotty/tree/master/compiler/src/dotty/tools/repl/terminal, it works well enough but does not support Windows. This has been recently fixed in Ammonite by using JLine 3 under Windows. We could merge these changes in our version of ammonite-terminal, but if we're going to depend on JLine anyway we could also drop our version of ammonite-terminal and just use JLine directly (unless there's some features of ammonite-terminal we really need).

[allanrenucci]

Here is the Ammonite PR for reference: com-lihaoyi/Ammonite#775

[Glavo]

I'm looking forward to using jline3 to implement dotty repl, because jline3's complement feature is very cool

[djx314]

+1 to use jline3 to support colourful output and mutiply lines coding in windows.

[Blaisorblade]

Renamed to help GitHub search find this: https://github.com/lampepfl/dotty/search?utf8=%E2%9C%93&q=repl+windows&type=Issues

[Glavo]

Now, there is still a problem with our Dotty REPL support for Chinese characters:
https://1drv.ms/v/s!Aj9QXHXa1Zz7jC_xz45zLZvrDPTw

Jline 3 can help us solve this problem:
https://1drv.ms/v/s!Aj9QXHXa1Zz7jDAjVfceTfqzMrZE

[Blaisorblade]

@Glavo Ah, so those are two characters but our REPL shows the cursor one character before it should be, as if they were one?

[Glavo]

@Blaisorblade Yes, and Ammonite also has this problem when not using the jline 3 front end.

[tisonkun]

As for the issue of Chinese characters, note that JLine's output transfer “你好” to its codepoint

[Blaisorblade]

As for the issue of Chinese characters, note that JLine's output transfer “你好” to its codepoint

@W4anD0eR96 Yes but I think that's a separate difference, independent from JLine and due to Ammonite's and Dotty's approaches at printing values — Dotty prints strings with toString (so "hi" prints hi, hence just print the actual content). Ammonite instead prints strings using PPrint, hence "hi" prints as "hi" and Unicode characters can be quoted.

[allanrenucci]

Fixed in #4680