src/Tools/Code/code_haskell.ML
changeset 34944 970e1466028d
parent 34269 b5c99df2e4b1
child 35228 ac2cab4583f4
equal deleted inserted replaced
34943:e97b22500a5c 34944:970e1466028d
   399 val literals = let
   399 val literals = let
   400   fun char_haskell c =
   400   fun char_haskell c =
   401     let
   401     let
   402       val s = ML_Syntax.print_char c;
   402       val s = ML_Syntax.print_char c;
   403     in if s = "'" then "\\'" else s end;
   403     in if s = "'" then "\\'" else s end;
       
   404   fun numeral_haskell k = if k >= 0 then string_of_int k
       
   405     else Library.enclose "(" ")" (signed_string_of_int k);
   404 in Literals {
   406 in Literals {
   405   literal_char = Library.enclose "'" "'" o char_haskell,
   407   literal_char = Library.enclose "'" "'" o char_haskell,
   406   literal_string = quote o translate_string char_haskell,
   408   literal_string = quote o translate_string char_haskell,
   407   literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
   409   literal_numeral = numeral_haskell,
   408     else Library.enclose "(" ")" (signed_string_of_int k),
   410   literal_positive_numeral = numeral_haskell,
       
   411   literal_naive_numeral = numeral_haskell,
   409   literal_list = enum "," "[" "]",
   412   literal_list = enum "," "[" "]",
   410   infix_cons = (5, ":")
   413   infix_cons = (5, ":")
   411 } end;
   414 } end;
   412 
   415 
   413 
   416