src/Tools/code/code_haskell.ML

--- a/src/Tools/code/code_haskell.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/Tools/code/code_haskell.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -408,6 +408,20 @@
       destination
   end;
 
+val literals = let
+  fun char_haskell c =
+    let
+      val s = ML_Syntax.print_char c;
+    in if s = "'" then "\\'" else s end;
+in Literals {
+  literal_char = enclose "'" "'" o char_haskell,
+  literal_string = quote o translate_string char_haskell,
+  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
+    else enclose "(" ")" (signed_string_of_int k),
+  literal_list = Pretty.enum "," "[" "]",
+  infix_cons = (5, ":")
+} end;
+
 
 (** optional monad syntax **)
 
@@ -474,7 +488,7 @@
   );
 
 val setup =
-  Code_Target.add_target (target, isar_seri_haskell)
+  Code_Target.add_target (target, (isar_seri_haskell, literals))
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,