when used in ide-mode idris sends wrongly formatted code (:browse-namespace)

[justjoheinz]

Steps to Reproduce

Use emacs or atom (browse namespace feature not released yet) Load some idris file and issue the M-x idris-browse-namespace command Choose e.g. Prelude.List as a namespace

Expected Behavior

functions which have type constraints, e.g. delete should have roughly the formatting

delete : Eq a => a -> List a -> List a

Observed Behavior

Instead idris sends the string

delete : Eq a -> a -> List a -> List a

(-> instead of =>)

Additional notes

I have not checked what happens if a function has multiple Type constraints. Are they becoming a paramater each?

[justjoheinz]

Please note that the error only occurs when using the ide-mode. Output in a Standard REPL is fine.

[melted]

Probably the fix is to use pprintDelabTy instead of pprintDelab on line 517 in Idris/REPL.hs like it is on line 1421 (where the CLIs version of browse is).

[conjunctive]

Fixed with PR https://github.com/idris-lang/Idris-dev/pull/4873