Output of String in REPL should be escaped

[glyh]

Steps to Reproduce

Evaluate "\"" in REPL

Expected Behavior

Outputs "\""

Observed Behavior

Output """

[gallais]

I think this is a duplicate of #759

[iacore]

@gallais I think this is fixed now.

Main> :exec putStrLn $ show "h\"a"
"h\"a"

Is it normal for Show String to escape the string rather than not change it? This feels like the need for two interfaces: like repr and str in Python.

[gallais]

It does seem to be fixed. A test case would be nice to ensure we don't introduce a regression.

[iacore]

I want to rewrite the test harness code first... why tests/Main.idr has every test's name

[gallais]

I want to rewrite the test harness code first... why tests/Main.idr has every test's name

This probably won't be accepted. Cf. #1736