tuned;
authorwenzelm
Mon, 23 Aug 2021 11:40:54 +0200
changeset 74169 43fe7388458f
parent 74168 f0b2136e2204
child 74170 09d4175f473e
tuned;
src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Aug 22 21:58:29 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Mon Aug 23 11:40:54 2021 +0200
@@ -3170,8 +3170,7 @@
           '\f' -> "$'\\f'"
           '\r' -> "$'\\r'"
           c ->
-            if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c == '+' || c == ',' ||
-              c == '-' || c == '.' || c == '/' || c == ':' || c == '_'
+            if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String)
             then Bytes.singleton b
             else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String)
             else "\\" <> Bytes.singleton b