diff -r 3533485fc7b8 -r d4a6460c53d1 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,