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

Merge pull request #1461 from david-christiansen/issue/1460

Browse Source 
Take .lidr syntax into account with :addmissing
This commit is contained in:
David Christiansen 2014-08-05 13:03:44 +02:00
commit 02f7c649ac
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Idris/Interactive.hs
View File

@ -28,6 +28,7 @@ import System.Directory
import System.IO
import Data.Char
import Data.Maybe (fromMaybe)
import Data.List (isSuffixOf)
import Debug.Trace
@ -122,10 +123,13 @@ addMissing fn updatefile l n
getAppName (PRef _ r) = r
getAppName _ = n
makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '
| otherwise = replicate ind ' '
showNew nm i ind (tm : tms)
= do (nm', i') <- getUniq nm i
rest <- showNew nm i' ind tms
return (replicate ind ' ' ++
return (makeIndent ind ++
showPat tm ++ " = ?" ++ nm' ++
"\n" ++ rest)
showNew nm i _ [] = return ""