New line after with in interactive mode
commit7412545c7a8d345f0b66e452e3c87a42b84f314b
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 18 Mar 2016, 18:21 (11 years ago)
parent1625765
src/Idris/Interactive.hs+1−1
@@ -172,7 +172,7 @@ makeWith fn updatefile l n
172172 ++ with ++ "\n" ++
173173 unlines rest)
174174 runIO $ copyFile fb fn
175− else iPrintResult with
175+ else iPrintResult (with ++ "\n")
176176 where getIndent s = length (takeWhile isSpace s)
177177
178178-- Replace the given metavariable on the given line with a 'case'
test/interactive001/expected+1
@@ -6,6 +6,7 @@ isElem x (y :: xs) = ?isElem_rhs_3
66f x :: map f xs
77isElem2 x (y :: ys) with (_)
88 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
9+
910 isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
1011
1112 [] => ?bar_1