ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 06:29:37 +03:00
Code Issues Projects Releases Wiki Activity

No newline after case in :makecase

Browse Source
This commit is contained in:
Edwin Brady 2015-08-28 18:08:36 +01:00
parent 378bbd6f98
commit 1e80f1f3cc
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/Interactive.hs
View File

@ -177,8 +177,8 @@ makeCase fn updatefile l n
Just (before, pos, after) ->
[before ++ (if b then "(" else "") ++ "case _ of",
take (pos + (if b then 6 else 5)) (repeat ' ') ++
"case_val => ?" ++ n ++ if b then ")" else "",
after]
"case_val => ?" ++ n ++ (if b then ")" else "")
++ after]
Nothing -> fail "No such metavariable"
-- Assume case needs to be bracketed unless the metavariable is