--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Haskell/File.hs Sat Nov 10 16:32:00 2018 +0100
@@ -0,0 +1,32 @@
+{- generated by Isabelle -}
+
+{- Title: Tools/Haskell/File.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+File-system operations
+-}
+
+module Isabelle.File (setup, read, write, append) where
+
+import Prelude hiding (read)
+import System.IO (IO)
+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)
--- a/src/Tools/Haskell/Haskell.thy Sat Nov 10 14:08:02 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Sat Nov 10 16:32:00 2018 +0100
@@ -516,6 +516,39 @@
no_output = ("", "")
\<close>
+generate_haskell_file "File.hs" = \<open>
+{- Title: Tools/Haskell/File.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+File-system operations
+-}
+
+module Isabelle.File (setup, read, write, append) where
+
+import Prelude hiding (read)
+import System.IO (IO)
+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)
+\<close>
+
generate_haskell_file "XML.hs" = \<open>
{- Title: Tools/Haskell/XML.hs
Author: Makarius