git.iko.soy/Idris-dev
on master help sign in
New line after with in interactive mode
7412545Edwin Brady
src/Idris/Interactive.hs+1−1
compare with master
unifiedsplit
@@ -172,7 +172,7 @@ makeWith fn updatefile l n
172 ++ with ++ "\n" ++
172 ++ with ++ "\n" ++
173 unlines rest)
173 unlines rest)
174 runIO $ copyFile fb fn
174 runIO $ copyFile fb fn
175− else iPrintResult with
175+ else iPrintResult (with ++ "\n")
176 where getIndent s = length (takeWhile isSpace s)
176 where getIndent s = length (takeWhile isSpace s)
177
177
178-- Replace the given metavariable on the given line with a 'case'
178-- 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
6f x :: map f xs
6f x :: map f xs
7isElem2 x (y :: ys) with (_)
7isElem2 x (y :: ys) with (_)
8 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
8 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
9+
9 isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
10 isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
10
11
11 [] => ?bar_1
12 [] => ?bar_1