# HG changeset patch
# User wenzelm
# Date 1629711654 -7200
# Node ID 43fe7388458fa2851a3370dba4078185f1955123
# Parent  f0b2136e2204ec21a34c0b686e5cf8ba378a83d8
tuned;

diff -r f0b2136e2204 -r 43fe7388458f 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