@@ -52,31 +52,18 @@ caseSplitAt fn updatefile l n
53addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
53addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
54addClauseFrom fn updatefile l n = do
54addClauseFrom fn updatefile l n = do
56− runIO . traceIO $ "addClauseFrom: " ++ show (M.fromList
58− , ("updatefile", show updatefile)
63 -- if a definition already exists, add missing cases rather than
55 -- if a definition already exists, add missing cases rather than
64 -- adding a new definition.
56 -- adding a new definition.
65 ist <- getIState
57 ist <- getIState
66 cl <- getInternalApp fn l
58 cl <- getInternalApp fn l
67−-- runIO . traceIO $ "cl = " ++ show cl
68 let fulln = getAppName cl
59 let fulln = getAppName cl
69−-- runIO . traceIO $ "fulln = " ++ show fulln
71 let metavars = lookup fulln (idris_metavars ist)
60 let metavars = lookup fulln (idris_metavars ist)
72−-- runIO . traceIO $ "metavars = " ++ show metavars
73 case metavars of
61 case metavars of
74 Nothing -> addMissing fn updatefile l n
62 Nothing -> addMissing fn updatefile l n
75 Just _ -> do
63 Just _ -> do
76 src <- runIO $ readSource fn
64 src <- runIO $ readSource fn
77 let (before, tyline : later) = splitAt (l-1) (lines src)
65 let (before, tyline : later) = splitAt (l-1) (lines src)
78 let indent = getIndent 0 (show n) tyline
66 let indent = getIndent 0 (show n) tyline
79−-- runIO . traceIO $ "getIndent => " ++ show indent
80 cl <- getClause l fulln n fn
67 cl <- getClause l fulln n fn
81 -- add clause before first blank line in 'later'
68 -- add clause before first blank line in 'later'
82 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
69 let (nonblank, rest) = span (not . all isSpace) (tyline:later)