4dd164c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Set encoding for read files.

It may seem strange to open a file and not close it, but that is how readFile works too. hGetContents is lazy and will close the file when all content has been read.

commit4dd164cac8454fae26885909660319c65f43915b authorNiklas Larsson <niklas@mm.st> dateThu 2 Apr 2015, 13:57 (12 years ago) parent663c401

5 files changed+33−21

compare with master

unifiedsplit

src/Idris/Chaser.hs+2−1 src/Idris/Interactive.hs+15−16 src/Idris/Parser.hs+2−1 src/Idris/REPL.hs+2−2 src/Util/System.hs+12−1

src/Idris/Chaser.hs+2−1

@@ -15,6 +15,7 @@ import Control.Monad.State

1515import Data.List

1616

1717import Debug.Trace

18+import Util.System (readSource, writeSource)

1819

1920data ModuleTree = MTree { mod_path :: IFileType,

2021 mod_needsRecheck :: Bool,

@@ -133,7 +134,7 @@ buildTree built fp = btree [] fp

133134 children lit f done = -- idrisCatch

134135 do exist <- runIO $ doesFileExist f

135136 if exist then do

136− file_in <- runIO $ readFile f

137+ file_in <- runIO $ readSource f

137138 file <- if lit then tclift $ unlit f file_in else return file_in

138139 (_, _, modules, _) <- parseImports f file

139140 -- The chaser should never report warnings from sub-modules

src/Idris/Interactive.hs+15−16

@@ -17,7 +17,6 @@ import Idris.Error

1717import Idris.Delaborate

1818import Idris.Output

1919import Idris.IdeMode hiding (IdeModeCommand(..))

20−

2120import Idris.Elab.Value

2221

2322import Util.Pretty

@@ -34,7 +33,7 @@ import Debug.Trace

3433

3534caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

3635caseSplitAt fn updatefile l n

37− = do src <- runIO $ readFile fn

36+ = do src <- runIO $ readSource fn

3837 res <- splitOnLine l n fn

3938 iLOG (showSep "\n" (map show res))

4039 let (before, (ap : later)) = splitAt (l-1) (lines src)

@@ -42,14 +41,14 @@ caseSplitAt fn updatefile l n

4241 let new = concat res'

4342 if updatefile

4443 then do let fb = fn ++ "~" -- make a backup!

45− runIO $ writeFile fb (unlines before ++ new ++ unlines later)

44+ runIO $ writeSource fb (unlines before ++ new ++ unlines later)

4645 runIO $ copyFile fb fn

4746 else -- do iputStrLn (show res)

4847 iPrintResult new

4948

5049addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

5150addClauseFrom fn updatefile l n

52− = do src <- runIO $ readFile fn

51+ = do src <- runIO $ readSource fn

5352 let (before, tyline : later) = splitAt (l-1) (lines src)

5453 let indent = getIndent 0 (show n) tyline

5554 cl <- getClause l n fn

@@ -57,7 +56,7 @@ addClauseFrom fn updatefile l n

5756 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

5857 if updatefile

5958 then do let fb = fn ++ "~"

60− runIO $ writeFile fb (unlines (before ++ nonblank) ++

59+ runIO $ writeSource fb (unlines (before ++ nonblank) ++

6160 replicate indent ' ' ++

6261 cl ++ "\n" ++

6362 unlines rest)

@@ -71,7 +70,7 @@ addClauseFrom fn updatefile l n

7170

7271addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

7372addProofClauseFrom fn updatefile l n

74− = do src <- runIO $ readFile fn

73+ = do src <- runIO $ readSource fn

7574 let (before, tyline : later) = splitAt (l-1) (lines src)

7675 let indent = getIndent 0 (show n) tyline

7776 cl <- getProofClause l n fn

@@ -79,7 +78,7 @@ addProofClauseFrom fn updatefile l n

7978 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

8079 if updatefile

8180 then do let fb = fn ++ "~"

82− runIO $ writeFile fb (unlines (before ++ nonblank) ++

81+ runIO $ writeSource fb (unlines (before ++ nonblank) ++

8382 replicate indent ' ' ++

8483 cl ++ "\n" ++

8584 unlines rest)

@@ -92,7 +91,7 @@ addProofClauseFrom fn updatefile l n

9291

9392addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

9493addMissing fn updatefile l n

95− = do src <- runIO $ readFile fn

94+ = do src <- runIO $ readSource fn

9695 let (before, tyline : later) = splitAt (l-1) (lines src)

9796 let indent = getIndent 0 (show n) tyline

9897 i <- getIState

@@ -106,7 +105,7 @@ addMissing fn updatefile l n

106105 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

107106 if updatefile

108107 then do let fb = fn ++ "~"

109− runIO $ writeFile fb (unlines (before ++ nonblank)

108+ runIO $ writeSource fb (unlines (before ++ nonblank)

110109 ++ extras ++ unlines rest)

111110 runIO $ copyFile fb fn

112111 else iPrintResult extras

@@ -141,7 +140,7 @@ addMissing fn updatefile l n

141140

142141makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

143142makeWith fn updatefile l n

144− = do src <- runIO $ readFile fn

143+ = do src <- runIO $ readSource fn

145144 let (before, tyline : later) = splitAt (l-1) (lines src)

146145 let ind = getIndent tyline

147146 let with = mkWith tyline n

@@ -151,7 +150,7 @@ makeWith fn updatefile l n

151150 not (ind == getIndent x)) later

152151 if updatefile then

153152 do let fb = fn ++ "~"

154− runIO $ writeFile fb (unlines (before ++ nonblank)

153+ runIO $ writeSource fb (unlines (before ++ nonblank)

155154 ++ with ++ "\n" ++

156155 unlines rest)

157156 runIO $ copyFile fb fn

@@ -164,7 +163,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->

164163doProofSearch fn updatefile rec l n hints Nothing

165164 = doProofSearch fn updatefile rec l n hints (Just 10)

166165doProofSearch fn updatefile rec l n hints (Just depth)

167− = do src <- runIO $ readFile fn

166+ = do src <- runIO $ readSource fn

168167 let (before, tyline : later) = splitAt (l-1) (lines src)

169168 ctxt <- getContext

170169 mn <- case lookupNames n ctxt of

@@ -192,7 +191,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

192191 (\e -> return ("?" ++ show n))

193192 if updatefile then

194193 do let fb = fn ++ "~"

195− runIO $ writeFile fb (unlines before ++

194+ runIO $ writeSource fb (unlines before ++

196195 updateMeta False tyline (show n) newmv ++ "\n"

197196 ++ unlines later)

198197 runIO $ copyFile fb fn

@@ -241,7 +240,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"

241240

242241makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()

243242makeLemma fn updatefile l n

244− = do src <- runIO $ readFile fn

243+ = do src <- runIO $ readSource fn

245244 let (before, tyline : later) = splitAt (l-1) (lines src)

246245

247246 -- if the name is in braces, rather than preceded by a ?, treat it

@@ -267,7 +266,7 @@ makeLemma fn updatefile l n

267266

268267 if updatefile then

269268 do let fb = fn ++ "~"

270− runIO $ writeFile fb (addLem before tyline lem lem_app later)

269+ runIO $ writeSource fb (addLem before tyline lem lem_app later)

271270 runIO $ copyFile fb fn

272271 else case idris_outputmode i of

273272 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app

@@ -285,7 +284,7 @@ makeLemma fn updatefile l n

285284 " = ?" ++ show n ++ "_rhs"

286285 if updatefile then

287286 do let fb = fn ++ "~"

288− runIO $ writeFile fb (addProv before tyline lem_app later)

287+ runIO $ writeSource fb (addProv before tyline lem_app later)

289288 runIO $ copyFile fb fn

290289 else case idris_outputmode i of

291290 RawOutput _ -> iPrintResult $ lem_app

src/Idris/Parser.hs+2−1

@@ -43,6 +43,7 @@ import Idris.Docstrings hiding (Unchecked)

4343import Paths_idris

4444

4545import Util.DynamicLinker

46+import Util.System (readSource, writeSource)

4647import qualified Util.Pretty as P

4748

4849import Idris.Core.TT

@@ -1345,7 +1346,7 @@ loadSource lidr f toline

13451346 = do iLOG ("Reading " ++ f)

13461347 i <- getIState

13471348 let def_total = default_total i

1348− file_in <- runIO $ readFile f

1349+ file_in <- runIO $ readSource f

13491350 file <- if lidr then tclift $ unlit f file_in else return file_in

13501351 (mdocs, mname, imports_in, pos) <- parseImports f file

13511352 ai <- getAutoImports

src/Idris/REPL.hs+2−2

@@ -1059,7 +1059,7 @@ process fn' (AddProof prf)

10591059 else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"

10601060 let fb = fn ++ "~"

10611061 runIO $ copyFile fn fb -- make a backup in case something goes wrong!

1062− prog <- runIO $ readFile fb

1062+ prog <- runIO $ readSource fb

10631063 i <- getIState

10641064 let proofs = proof_list i

10651065 n' <- case prf of

@@ -1071,7 +1071,7 @@ process fn' (AddProof prf)

10711071 case lookup n proofs of

10721072 Nothing -> iputStrLn "No proof to add"

10731073 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls

1074− runIO $ writeFile fn (unlines prog')

1074+ runIO $ writeSource fn (unlines prog')

10751075 removeProof n

10761076 iputStrLn $ "Added proof " ++ show n

10771077 where ls = (lines prog)

src/Util/System.hs+12−1

@@ -1,4 +1,5 @@

1−module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows) where

1+module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,

2+ readSource, writeSource) where

34-- System helper functions.

45import Control.Monad (when)

@@ -26,6 +27,16 @@ tempfile :: IO (FilePath, Handle)

2627tempfile = do dir <- getTemporaryDirectory

2728 openTempFile (normalise dir) "idris"

2829

30+-- | Read a source file, same as readFile but make sure the encoding is utf-8.

31+readSource :: FilePath -> IO String

32+readSource f = do h <- openFile f ReadMode

33+ hSetEncoding h utf8

34+ hGetContents h

35+

36+-- | Write a source file, same as writeFile except the encoding is set to utf-8

37+writeSource :: FilePath -> String -> IO ()

38+writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)

39+

2940withTempdir :: String -> (FilePath -> IO a) -> IO a

3041withTempdir subdir callback

3142 = do dir <- getTemporaryDirectory