@@ -590,12 +590,14 @@ process h fn (AddProofClauseFrom updatefile l n)
590590process h fn (AddMissing updatefile l n)
591591 = do src <- runIO $ readFile fn
592592 let (before, tyline : later) = splitAt (l-1) (lines src)
593+ let indent = getIndent 0 (show n) tyline
593594 i <- getIState
594595 cl <- getInternalApp fn l
595596 let n' = getAppName cl
597+
596598 extras <- case lookupCtxt n' (idris_patdefs i) of
597599 [] -> return ""
598− [(_, tms)] -> showNew (show n ++ "_rhs") 1 tms
600+ [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms
599601 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
600602 if updatefile then
601603 do let fb = fn ++ "~"
@@ -616,12 +618,17 @@ process h fn (AddMissing updatefile l n)
616618 getAppName (PRef _ r) = r
617619 getAppName _ = n
618620
619− showNew nm i (tm : tms)
621+ showNew nm i ind (tm : tms)
620622 = do (nm', i') <- getUniq nm i
621− rest <- showNew nm i' tms
622− return (showPat tm ++ " = ?" ++ nm' ++
623+ rest <- showNew nm i' ind tms
624+ return (replicate ind ' ' ++
625+ showPat tm ++ " = ?" ++ nm' ++
623626 "\n" ++ rest)
624− showNew nm i [] = return ""
627+ showNew nm i _ [] = return ""
628+
629+ getIndent i n [] = 0
630+ getIndent i n xs | take (length n) xs == n = i
631+ getIndent i n (x : xs) = getIndent (i + 1) n xs
625632
626633process h fn (MakeWith updatefile l n)
627634 = do src <- runIO $ readFile fn