clarified signature;
authorwenzelm
Sun, 01 Aug 2021 16:12:08 +0200
changeset 74362 5aaccec7c1a1
parent 74361 6d7be1227d02
child 74363 0bda15b1b937
clarified signature;
src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Aug 01 10:20:34 2021 +0000
+++ b/src/Tools/Haskell/Haskell.thy	Sun Aug 01 16:12:08 2021 +0200
@@ -153,10 +153,12 @@
 {-# LANGUAGE InstanceSigs #-}
 
 module Isabelle.UTF8 (
+  setup, setup3,
   Recode (..)
 )
 where
 
+import qualified System.IO as IO
 import Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Text.Encoding as Encoding
@@ -167,6 +169,16 @@
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 
+setup :: IO.Handle -> IO ()
+setup h = do
+  IO.hSetEncoding h IO.utf8
+  IO.hSetNewlineMode h IO.noNewlineTranslation
+
+setup3 :: IO.Handle -> IO.Handle -> IO.Handle -> IO ()
+setup3 h1 h2 h3 = do
+  setup h1
+  setup h2
+  setup h3
 
 class Recode a b where
   encode :: a -> b
@@ -1561,28 +1573,22 @@
 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
 -}
 
-module Isabelle.File (setup, read, write, append) where
+module Isabelle.File (read, write, append) where
 
 import Prelude hiding (read)
 import qualified System.IO as IO
-
-setup :: IO.Handle -> IO ()
-setup h = do
-  IO.hSetEncoding h IO.utf8
-  IO.hSetNewlineMode h IO.noNewlineTranslation
-
-read :: IO.FilePath -> IO String
-read path =
-  IO.withFile path IO.ReadMode (\h ->
-    do setup h; IO.hGetContents h >>= \s -> length s `seq` return s)
-
-write :: IO.FilePath -> String -> IO ()
-write path s =
-  IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s)
-
-append :: IO.FilePath -> String -> IO ()
-append path s =
-  IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
+import qualified Data.ByteString as ByteString
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+
+read :: IO.FilePath -> IO Bytes
+read path = Bytes.make <$> IO.withFile path IO.ReadMode ByteString.hGetContents
+
+write :: IO.FilePath -> Bytes -> IO ()
+write path bs = IO.withFile path IO.WriteMode (\h -> ByteString.hPut h (Bytes.unmake bs))
+
+append :: IO.FilePath -> Bytes -> IO ()
+append path bs = IO.withFile path IO.AppendMode (\h -> ByteString.hPut h (Bytes.unmake bs))
 \<close>
 
 generate_file "Isabelle/Pretty.hs" = \<open>