1.1 --- a/src/Tools/code/code_target.ML Thu Mar 27 19:04:41 2008 +0100
1.2 +++ b/src/Tools/code/code_target.ML Thu Mar 27 19:04:42 2008 +0100
1.3 @@ -1737,6 +1737,23 @@
1.4
1.5 local
1.6
1.7 +fun ocaml_char c =
1.8 + let
1.9 + fun chr i =
1.10 + let
1.11 + val xs = string_of_int i;
1.12 + val ys = replicate_string (3 - length (explode xs)) "0";
1.13 + in "\\" ^ ys ^ xs end;
1.14 + val i = ord c;
1.15 + val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
1.16 + then chr i else c
1.17 + in s end;
1.18 +
1.19 +fun haskell_char c =
1.20 + let
1.21 + val s = ML_Syntax.print_char c;
1.22 + in if s = "'" then "\\'" else s end;
1.23 +
1.24 val pretty : (string * {
1.25 pretty_char: string -> string,
1.26 pretty_string: string -> string,
1.27 @@ -1745,19 +1762,14 @@
1.28 infix_cons: int * string
1.29 }) list = [
1.30 ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
1.31 - pretty_string = ML_Syntax.print_string,
1.32 + pretty_string = quote o translate_string ML_Syntax.print_char,
1.33 pretty_numeral = fn unbounded => fn k =>
1.34 if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
1.35 else string_of_int k,
1.36 pretty_list = Pretty.enum "," "[" "]",
1.37 infix_cons = (7, "::")}),
1.38 - ("OCaml", { pretty_char = fn c => enclose "'" "'"
1.39 - (let val i = ord c
1.40 - in if i < 32 orelse i = 39 orelse i = 92
1.41 - then prefix "\\" (string_of_int i)
1.42 - else c
1.43 - end),
1.44 - pretty_string = ML_Syntax.print_string,
1.45 + ("OCaml", { pretty_char = enclose "'" "'" o ocaml_char,
1.46 + pretty_string = quote o translate_string ocaml_char,
1.47 pretty_numeral = fn unbounded => fn k => if k >= 0 then
1.48 if unbounded then
1.49 "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
1.50 @@ -1769,13 +1781,8 @@
1.51 else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
1.52 pretty_list = Pretty.enum ";" "[" "]",
1.53 infix_cons = (6, "::")}),
1.54 - ("Haskell", { pretty_char = fn c => enclose "'" "'"
1.55 - (let val i = ord c
1.56 - in if i < 32 orelse i = 39 orelse i = 92
1.57 - then Library.prefix "\\" (string_of_int i)
1.58 - else c
1.59 - end),
1.60 - pretty_string = ML_Syntax.print_string,
1.61 + ("Haskell", { pretty_char = enclose "'" "'" o haskell_char,
1.62 + pretty_string = quote o translate_string haskell_char,
1.63 pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
1.64 else enclose "(" ")" (signed_string_of_int k),
1.65 pretty_list = Pretty.enum "," "[" "]",
1.66 @@ -1813,9 +1820,9 @@
1.67 val mk_string = #pretty_string pretty_ops;
1.68 fun pretty pr vars fxy [(t1, _), (t2, _)] =
1.69 case Option.map (cons t1) (implode_list c_nil c_cons t2)
1.70 - of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
1.71 + of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
1.72 of SOME p => p
1.73 - | NONE => mk_list (map (pr vars NOBR) ts)
1.74 + | NONE => mk_list (map (pr vars NOBR) ts))
1.75 | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
1.76 in (2, pretty) end;
1.77