@@ -37,7 +37,7 @@ import System.IO
3737
3838caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
3939caseSplitAt fn updatefile l n
40− = do src <- runIO $ readSource fn
40+ = do src <- runIO $ readSourceStrict fn
4141 (ok, res) <- splitOnLine l n fn
4242 logLvl 1 (showSep "\n" (map show res))
4343 let (before, (ap : later)) = splitAt (l-1) (lines src)
@@ -61,7 +61,7 @@ addClauseFrom fn updatefile l n = do
6161 case metavars of
6262 Nothing -> addMissing fn updatefile l n
6363 Just _ -> do
64− src <- runIO $ readSource fn
64+ src <- runIO $ readSourceStrict fn
6565 let (before, tyline : later) = splitAt (l-1) (lines src)
6666 let indent = getIndent 0 (show n) tyline
6767 cl <- getClause l fulln n fn
@@ -88,7 +88,7 @@ addClauseFrom fn updatefile l n = do
8888
8989addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
9090addProofClauseFrom fn updatefile l n
91− = do src <- runIO $ readSource fn
91+ = do src <- runIO $ readSourceStrict fn
9292 let (before, tyline : later) = splitAt (l-1) (lines src)
9393 let indent = getIndent 0 (show n) tyline
9494 cl <- getProofClause l n fn
@@ -109,7 +109,7 @@ addProofClauseFrom fn updatefile l n
109109
110110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111111addMissing fn updatefile l n
112− = do src <- runIO $ readSource fn
112+ = do src <- runIO $ readSourceStrict fn
113113 let (before, tyline : later) = splitAt (l-1) (lines src)
114114 let indent = getIndent tyline
115115 i <- getIState
@@ -127,7 +127,7 @@ addMissing fn updatefile l n
127127 ++ extras
128128 ++ (if null extras then "" else "\n")
129129 ++ unlines rest)
130− runIO $ copyFile fb fn
130+ runIO $ (length src `seq` copyFile fb fn)
131131 else iPrintResult extras
132132 where showPat = show . stripNS
133133 stripNS tm = mapPT dens tm where
@@ -160,7 +160,7 @@ addMissing fn updatefile l n
160160
161161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
162162makeWith fn updatefile l n = do
163− src <- runIO $ readSource fn
163+ src <- runIO $ readSourceStrict fn
164164 i <- getIState
165165 indentWith <- getIndentWith
166166 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -184,7 +184,7 @@ makeWith fn updatefile l n = do
184184-- block, using a _ for the scrutinee
185185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
186186makeCase fn updatefile l n
187− = do src <- runIO $ readSource fn
187+ = do src <- runIO $ readSourceStrict fn
188188 let (before, tyline : later) = splitAt (l-1) (lines src)
189189 let newcase = addCaseSkel (show n) tyline
190190
@@ -224,7 +224,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->
224224doProofSearch fn updatefile rec l n hints Nothing
225225 = doProofSearch fn updatefile rec l n hints (Just 20)
226226doProofSearch fn updatefile rec l n hints (Just depth)
227− = do src <- runIO $ readSource fn
227+ = do src <- runIO $ readSourceStrict fn
228228 let (before, tyline : later) = splitAt (l-1) (lines src)
229229 ctxt <- getContext
230230 mn <- case lookupNames n ctxt of
@@ -319,7 +319,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"
319319
320320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
321321makeLemma fn updatefile l n
322− = do src <- runIO $ readSource fn
322+ = do src <- runIO $ readSourceStrict fn
323323 let (before, tyline : later) = splitAt (l-1) (lines src)
324324
325325 -- if the name is in braces, rather than preceded by a ?, treat it