tuned -- prefer GHC.print_codepoint;
authorwenzelm
Tue, 30 Oct 2018 19:25:32 +0100
changeset 69210 92fde8f61b0d
parent 69209 3f4210c13356
child 69211 7062639cfdaa
tuned -- prefer GHC.print_codepoint;
src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Oct 30 19:18:01 2018 +0100
+++ b/src/Tools/Code/code_haskell.ML	Tue Oct 30 19:25:32 2018 +0100
@@ -36,14 +36,9 @@
 (** Haskell serializer **)
 
 val print_haskell_string =
-  let
-    fun char c =
-      let
-        val _ = if Symbol.is_ascii c then ()
-          else error "non-ASCII byte in Haskell string literal";
-        val s = ML_Syntax.print_symbol_char c;
-      in if s = "'" then "\\'" else s end;
-  in quote o translate_string char end;
+  quote o translate_string (fn c =>
+    if Symbol.is_ascii c then GHC.print_codepoint (ord c)
+    else error "non-ASCII byte in Haskell string literal");
 
 fun print_haskell_stmt class_syntax tyco_syntax const_syntax
     reserved deresolve deriving_show =