--- a/src/Tools/Haskell/Haskell.thy Fri Jul 30 23:00:50 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Sat Jul 31 11:40:37 2021 +0200
@@ -19,6 +19,8 @@
and \<^file>\<open>$ISABELLE_HOME/src/Pure/General/bytes.scala\<close>.
-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
module Isabelle.Bytes (
Bytes,
make, unmake, pack, unpack,
@@ -85,12 +87,12 @@
trim_line :: Bytes -> Bytes
trim_line s =
- if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then take (n - 2) s
- else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then take (n - 1) s
+ if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then take (n - 2) s
+ else if n >= 1 && (at (n - 1) == '\r' || at (n - 1) == '\n') then take (n - 1) s
else s
where
n = length s
- at = index s
+ at :: Int -> Char = toEnum . fromEnum . index s
\<close>
generate_file "Isabelle/UTF8.hs" = \<open>