clarified character serializations
authorhaftmann
Thu Mar 27 19:04:42 2008 +0100 (2008-03-27)
changeset 26448faf056ac64c4
parent 26447 fef9dde61a46
child 26449 283107142592
clarified character serializations
src/Tools/code/code_target.ML
     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