@@ -37,7 +37,7 @@ import System.IO
38caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
38caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
39caseSplitAt fn updatefile l n
39caseSplitAt fn updatefile l n
40− = do src <- runIO $ readSource fn
40+ = do src <- runIO $ readSourceStrict fn
41 (ok, res) <- splitOnLine l n fn
41 (ok, res) <- splitOnLine l n fn
42 logLvl 1 (showSep "\n" (map show res))
42 logLvl 1 (showSep "\n" (map show res))
43 let (before, (ap : later)) = splitAt (l-1) (lines src)
43 let (before, (ap : later)) = splitAt (l-1) (lines src)
@@ -61,7 +61,7 @@ addClauseFrom fn updatefile l n = do
61 case metavars of
61 case metavars of
62 Nothing -> addMissing fn updatefile l n
62 Nothing -> addMissing fn updatefile l n
63 Just _ -> do
63 Just _ -> do
64− src <- runIO $ readSource fn
64+ src <- runIO $ readSourceStrict fn
65 let (before, tyline : later) = splitAt (l-1) (lines src)
65 let (before, tyline : later) = splitAt (l-1) (lines src)
66 let indent = getIndent 0 (show n) tyline
66 let indent = getIndent 0 (show n) tyline
67 cl <- getClause l fulln n fn
67 cl <- getClause l fulln n fn
@@ -88,7 +88,7 @@ addClauseFrom fn updatefile l n = do
89addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
89addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
90addProofClauseFrom fn updatefile l n
90addProofClauseFrom fn updatefile l n
91− = do src <- runIO $ readSource fn
91+ = do src <- runIO $ readSourceStrict fn
92 let (before, tyline : later) = splitAt (l-1) (lines src)
92 let (before, tyline : later) = splitAt (l-1) (lines src)
93 let indent = getIndent 0 (show n) tyline
93 let indent = getIndent 0 (show n) tyline
94 cl <- getProofClause l n fn
94 cl <- getProofClause l n fn
@@ -109,7 +109,7 @@ addProofClauseFrom fn updatefile l n
110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111addMissing fn updatefile l n
111addMissing fn updatefile l n
112− = do src <- runIO $ readSource fn
112+ = do src <- runIO $ readSourceStrict fn
113 let (before, tyline : later) = splitAt (l-1) (lines src)
113 let (before, tyline : later) = splitAt (l-1) (lines src)
114 let indent = getIndent tyline
114 let indent = getIndent tyline
115 i <- getIState
115 i <- getIState
@@ -127,7 +127,7 @@ addMissing fn updatefile l n
127 ++ extras
127 ++ extras
128 ++ (if null extras then "" else "\n")
128 ++ (if null extras then "" else "\n")
129 ++ unlines rest)
129 ++ unlines rest)
130− runIO $ copyFile fb fn
130+ runIO $ (length src `seq` copyFile fb fn)
131 else iPrintResult extras
131 else iPrintResult extras
132 where showPat = show . stripNS
132 where showPat = show . stripNS
133 stripNS tm = mapPT dens tm where
133 stripNS tm = mapPT dens tm where
@@ -160,7 +160,7 @@ addMissing fn updatefile l n
161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
162makeWith fn updatefile l n = do
162makeWith fn updatefile l n = do
163− src <- runIO $ readSource fn
163+ src <- runIO $ readSourceStrict fn
164 i <- getIState
164 i <- getIState
165 indentWith <- getIndentWith
165 indentWith <- getIndentWith
166 let (before, tyline : later) = splitAt (l-1) (lines src)
166 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -184,7 +184,7 @@ makeWith fn updatefile l n = do
184-- block, using a _ for the scrutinee
184-- block, using a _ for the scrutinee
185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
186makeCase fn updatefile l n
186makeCase fn updatefile l n
187− = do src <- runIO $ readSource fn
187+ = do src <- runIO $ readSourceStrict fn
188 let (before, tyline : later) = splitAt (l-1) (lines src)
188 let (before, tyline : later) = splitAt (l-1) (lines src)
189 let newcase = addCaseSkel (show n) tyline
189 let newcase = addCaseSkel (show n) tyline
@@ -224,7 +224,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->
224doProofSearch fn updatefile rec l n hints Nothing
224doProofSearch fn updatefile rec l n hints Nothing
225 = doProofSearch fn updatefile rec l n hints (Just 20)
225 = doProofSearch fn updatefile rec l n hints (Just 20)
226doProofSearch fn updatefile rec l n hints (Just depth)
226doProofSearch fn updatefile rec l n hints (Just depth)
227− = do src <- runIO $ readSource fn
227+ = do src <- runIO $ readSourceStrict fn
228 let (before, tyline : later) = splitAt (l-1) (lines src)
228 let (before, tyline : later) = splitAt (l-1) (lines src)
229 ctxt <- getContext
229 ctxt <- getContext
230 mn <- case lookupNames n ctxt of
230 mn <- case lookupNames n ctxt of
@@ -319,7 +319,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"
320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
321makeLemma fn updatefile l n
321makeLemma fn updatefile l n
322− = do src <- runIO $ readSource fn
322+ = do src <- runIO $ readSourceStrict fn
323 let (before, tyline : later) = splitAt (l-1) (lines src)
323 let (before, tyline : later) = splitAt (l-1) (lines src)
325 -- if the name is in braces, rather than preceded by a ?, treat it
325 -- if the name is in braces, rather than preceded by a ?, treat it