@@ -52,31 +52,18 @@ caseSplitAt fn updatefile l n
5252
5353addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
5454addClauseFrom fn updatefile l n = do
55−{-
56− runIO . traceIO $ "addClauseFrom: " ++ show (M.fromList
57− [ ("fn", fn)
58− , ("updatefile", show updatefile)
59− , ("line", show l)
60− , ("name", show n)
61− ])
62−-}
6355 -- if a definition already exists, add missing cases rather than
6456 -- adding a new definition.
6557 ist <- getIState
6658 cl <- getInternalApp fn l
67−-- runIO . traceIO $ "cl = " ++ show cl
6859 let fulln = getAppName cl
69−-- runIO . traceIO $ "fulln = " ++ show fulln
70−
7160 let metavars = lookup fulln (idris_metavars ist)
72−-- runIO . traceIO $ "metavars = " ++ show metavars
7361 case metavars of
7462 Nothing -> addMissing fn updatefile l n
7563 Just _ -> do
7664 src <- runIO $ readSource fn
7765 let (before, tyline : later) = splitAt (l-1) (lines src)
7866 let indent = getIndent 0 (show n) tyline
79−-- runIO . traceIO $ "getIndent => " ++ show indent
8067 cl <- getClause l fulln n fn
8168 -- add clause before first blank line in 'later'
8269 let (nonblank, rest) = span (not . all isSpace) (tyline:later)