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

git.iko.soy/Idris-dev

on master help sign in

Set encoding for read files.

4dd164cNiklas Larsson12 years ago

src/Idris/Chaser.hs+2−1

compare with master

unifiedsplit

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

15import Data.List

17import Debug.Trace

18+import Util.System (readSource, writeSource)

19data ModuleTree = MTree { mod_path :: IFileType,

20data ModuleTree = MTree { mod_path :: IFileType,

20 mod_needsRecheck :: Bool,

21 mod_needsRecheck :: Bool,

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

133 children lit f done = -- idrisCatch

134 children lit f done = -- idrisCatch

134 do exist <- runIO $ doesFileExist f

135 do exist <- runIO $ doesFileExist f

135 if exist then do

136 if exist then do

136− file_in <- runIO $ readFile f

137+ file_in <- runIO $ readSource f

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

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

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

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

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

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

src/Idris/Interactive.hs+15−16

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

17import Idris.Delaborate

18import Idris.Output

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

20−

21import Idris.Elab.Value

20import Idris.Elab.Value

23import Util.Pretty

22import Util.Pretty

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

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

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

36caseSplitAt fn updatefile l n

35caseSplitAt fn updatefile l n

37− = do src <- runIO $ readFile fn

36+ = do src <- runIO $ readSource fn

38 res <- splitOnLine l n fn

37 res <- splitOnLine l n fn

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

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

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

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

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

42 let new = concat res'

41 let new = concat res'

43 if updatefile

42 if updatefile

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

43 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)

46 runIO $ copyFile fb fn

45 runIO $ copyFile fb fn

47 else -- do iputStrLn (show res)

46 else -- do iputStrLn (show res)

48 iPrintResult new

47 iPrintResult new

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

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

51addClauseFrom fn updatefile l n

50addClauseFrom fn updatefile l n

52− = do src <- runIO $ readFile fn

51+ = do src <- runIO $ readSource fn

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

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

54 let indent = getIndent 0 (show n) tyline

53 let indent = getIndent 0 (show n) tyline

55 cl <- getClause l n fn

54 cl <- getClause l n fn

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

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

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

58 if updatefile

57 if updatefile

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

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

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

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

61 replicate indent ' ' ++

60 replicate indent ' ' ++

62 cl ++ "\n" ++

61 cl ++ "\n" ++

63 unlines rest)

62 unlines rest)

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

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

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

73addProofClauseFrom fn updatefile l n

72addProofClauseFrom fn updatefile l n

74− = do src <- runIO $ readFile fn

73+ = do src <- runIO $ readSource fn

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

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

76 let indent = getIndent 0 (show n) tyline

75 let indent = getIndent 0 (show n) tyline

77 cl <- getProofClause l n fn

76 cl <- getProofClause l n fn

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

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

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

80 if updatefile

79 if updatefile

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

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

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

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

83 replicate indent ' ' ++

82 replicate indent ' ' ++

84 cl ++ "\n" ++

83 cl ++ "\n" ++

85 unlines rest)

84 unlines rest)

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

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

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

94addMissing fn updatefile l n

93addMissing fn updatefile l n

95− = do src <- runIO $ readFile fn

94+ = do src <- runIO $ readSource fn

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

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

97 let indent = getIndent 0 (show n) tyline

96 let indent = getIndent 0 (show n) tyline

98 i <- getIState

97 i <- getIState

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

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

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

107 if updatefile

106 if updatefile

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

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

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

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

110 ++ extras ++ unlines rest)

109 ++ extras ++ unlines rest)

111 runIO $ copyFile fb fn

110 runIO $ copyFile fb fn

112 else iPrintResult extras

111 else iPrintResult extras

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

141

140

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

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

143makeWith fn updatefile l n

142makeWith fn updatefile l n

144− = do src <- runIO $ readFile fn

143+ = do src <- runIO $ readSource fn

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

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

146 let ind = getIndent tyline

145 let ind = getIndent tyline

147 let with = mkWith tyline n

146 let with = mkWith tyline n

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

151 not (ind == getIndent x)) later

150 not (ind == getIndent x)) later

152 if updatefile then

151 if updatefile then

153 do let fb = fn ++ "~"

152 do let fb = fn ++ "~"

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

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

155 ++ with ++ "\n" ++

154 ++ with ++ "\n" ++

156 unlines rest)

155 unlines rest)

157 runIO $ copyFile fb fn

156 runIO $ copyFile fb fn

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

164doProofSearch fn updatefile rec l n hints Nothing

163doProofSearch fn updatefile rec l n hints Nothing

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

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

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

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

167− = do src <- runIO $ readFile fn

166+ = do src <- runIO $ readSource fn

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

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

169 ctxt <- getContext

168 ctxt <- getContext

170 mn <- case lookupNames n ctxt of

169 mn <- case lookupNames n ctxt of

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

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

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

193 if updatefile then

192 if updatefile then

194 do let fb = fn ++ "~"

193 do let fb = fn ++ "~"

195− runIO $ writeFile fb (unlines before ++

194+ runIO $ writeSource fb (unlines before ++

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

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

197 ++ unlines later)

196 ++ unlines later)

198 runIO $ copyFile fb fn

197 runIO $ copyFile fb fn

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

241

240

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

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

243makeLemma fn updatefile l n

242makeLemma fn updatefile l n

244− = do src <- runIO $ readFile fn

243+ = do src <- runIO $ readSource fn

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

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

246

245

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

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

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

267

266

268 if updatefile then

267 if updatefile then

269 do let fb = fn ++ "~"

268 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)

271 runIO $ copyFile fb fn

270 runIO $ copyFile fb fn

272 else case idris_outputmode i of

271 else case idris_outputmode i of

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

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

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

285 " = ?" ++ show n ++ "_rhs"

284 " = ?" ++ show n ++ "_rhs"

286 if updatefile then

285 if updatefile then

287 do let fb = fn ++ "~"

286 do let fb = fn ++ "~"

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

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

289 runIO $ copyFile fb fn

288 runIO $ copyFile fb fn

290 else case idris_outputmode i of

289 else case idris_outputmode i of

291 RawOutput _ -> iPrintResult $ lem_app

290 RawOutput _ -> iPrintResult $ lem_app

src/Idris/Parser.hs+2−1

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

43import Paths_idris

45import Util.DynamicLinker

46+import Util.System (readSource, writeSource)

46import qualified Util.Pretty as P

47import qualified Util.Pretty as P

48import Idris.Core.TT

49import Idris.Core.TT

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

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

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

1346 i <- getIState

1347 i <- getIState

1347 let def_total = default_total i

1348 let def_total = default_total i

1348− file_in <- runIO $ readFile f

1349+ file_in <- runIO $ readSource f

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

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

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

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

1351 ai <- getAutoImports

1352 ai <- getAutoImports

src/Idris/REPL.hs+2−2

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

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

1060 let fb = fn ++ "~"

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

1062− prog <- runIO $ readFile fb

1062+ prog <- runIO $ readSource fb

1063 i <- getIState

1064 let proofs = proof_list i

1065 n' <- case prf of

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

1071 case lookup n proofs of

1072 Nothing -> iputStrLn "No proof to add"

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

1074− runIO $ writeFile fn (unlines prog')

1074+ runIO $ writeSource fn (unlines prog')

1075 removeProof n

1076 iputStrLn $ "Added proof " ++ show n

1077 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

3-- System helper functions.

4-- System helper functions.

4import Control.Monad (when)

5import Control.Monad (when)

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

26tempfile = do dir <- getTemporaryDirectory

27tempfile = do dir <- getTemporaryDirectory

27 openTempFile (normalise dir) "idris"

28 openTempFile (normalise dir) "idris"

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+

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

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

30withTempdir subdir callback

41withTempdir subdir callback

31 = do dir <- getTemporaryDirectory

42 = do dir <- getTemporaryDirectory