1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Aug 29 20:36:08 2008 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Mon Sep 01 10:18:37 2008 +0200
     1.3 @@ -36,9 +36,9 @@
     1.4      @{const_name NibbleC}, @{const_name NibbleD},
     1.5      @{const_name NibbleE}, @{const_name NibbleF}];
     1.6  in
     1.7 -  fold (fn target => Code_Target.add_pretty_char target charr nibbles)
     1.8 +  fold (fn target => Code_Target.add_literal_char target charr nibbles)
     1.9      ["SML", "OCaml", "Haskell"]
    1.10 -  #> Code_Target.add_pretty_list_string "Haskell"
    1.11 +  #> Code_Target.add_literal_list_string "Haskell"
    1.12      @{const_name Nil} @{const_name Cons} charr nibbles
    1.13  end
    1.14  *}

     2.1 --- a/src/HOL/Library/Code_Message.thy	Fri Aug 29 20:36:08 2008 +0200
     2.2 +++ b/src/HOL/Library/Code_Message.thy	Mon Sep 01 10:18:37 2008 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4      @{const_name NibbleC}, @{const_name NibbleD},
     2.5      @{const_name NibbleE}, @{const_name NibbleF}];
     2.6  in
     2.7 -  fold (fn target => Code_Target.add_pretty_message target
     2.8 +  fold (fn target => Code_Target.add_literal_message target
     2.9      charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
    2.10    ["SML", "OCaml", "Haskell"]
    2.11  end

     3.1 --- a/src/HOL/List.thy	Fri Aug 29 20:36:08 2008 +0200
     3.2 +++ b/src/HOL/List.thy	Mon Sep 01 10:18:37 2008 +0200
     3.3 @@ -3450,7 +3450,7 @@
     3.4    (Haskell "[]")
     3.5  
     3.6  setup {*
     3.7 -  fold (fn target => Code_Target.add_pretty_list target
     3.8 +  fold (fn target => Code_Target.add_literal_list target
     3.9      @{const_name Nil} @{const_name Cons}
    3.10    ) ["SML", "OCaml", "Haskell"]
    3.11  *}

     4.1 --- a/src/HOL/Tools/numeral.ML	Fri Aug 29 20:36:08 2008 +0200
     4.2 +++ b/src/HOL/Tools/numeral.ML	Mon Sep 01 10:18:37 2008 +0200
     4.3 @@ -56,7 +56,7 @@
     4.4  (* code generator *)
     4.5  
     4.6  fun add_code number_of negative unbounded target =
     4.7 -  Code_Target.add_pretty_numeral target negative unbounded number_of
     4.8 +  Code_Target.add_literal_numeral target negative unbounded number_of
     4.9    @{const_name Int.Pls} @{const_name Int.Min}
    4.10    @{const_name Int.Bit0} @{const_name Int.Bit1};
    4.11  

     5.1 --- a/src/Tools/code/code_haskell.ML	Fri Aug 29 20:36:08 2008 +0200
     5.2 +++ b/src/Tools/code/code_haskell.ML	Mon Sep 01 10:18:37 2008 +0200
     5.3 @@ -408,6 +408,20 @@
     5.4        destination
     5.5    end;
     5.6  
     5.7 +val literals = let
     5.8 +  fun char_haskell c =
     5.9 +    let
    5.10 +      val s = ML_Syntax.print_char c;
    5.11 +    in if s = "'" then "\\'" else s end;
    5.12 +in Literals {
    5.13 +  literal_char = enclose "'" "'" o char_haskell,
    5.14 +  literal_string = quote o translate_string char_haskell,
    5.15 +  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
    5.16 +    else enclose "(" ")" (signed_string_of_int k),
    5.17 +  literal_list = Pretty.enum "," "[" "]",
    5.18 +  infix_cons = (5, ":")
    5.19 +} end;
    5.20 +
    5.21  
    5.22  (** optional monad syntax **)
    5.23  
    5.24 @@ -474,7 +488,7 @@
    5.25    );
    5.26  
    5.27  val setup =
    5.28 -  Code_Target.add_target (target, isar_seri_haskell)
    5.29 +  Code_Target.add_target (target, (isar_seri_haskell, literals))
    5.30    #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
    5.31        brackify_infix (1, R) fxy [
    5.32          pr_typ (INFX (1, X)) ty1,

     6.1 --- a/src/Tools/code/code_ml.ML	Fri Aug 29 20:36:08 2008 +0200
     6.2 +++ b/src/Tools/code/code_ml.ML	Mon Sep 01 10:18:37 2008 +0200
     6.3 @@ -329,6 +329,16 @@
     6.4      @@ str ("end; (*struct " ^ name ^ "*)")
     6.5    );
     6.6  
     6.7 +val literals_sml = Literals {
     6.8 +  literal_char = prefix "#" o quote o ML_Syntax.print_char,
     6.9 +  literal_string = quote o translate_string ML_Syntax.print_char,
    6.10 +  literal_numeral = fn unbounded => fn k =>
    6.11 +    if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
    6.12 +    else string_of_int k,
    6.13 +  literal_list = Pretty.enum "," "[" "]",
    6.14 +  infix_cons = (7, "::")
    6.15 +};
    6.16 +
    6.17  
    6.18  (** OCaml serializer **)
    6.19  
    6.20 @@ -633,6 +643,35 @@
    6.21      @@ str ("end;; (*struct " ^ name ^ "*)")
    6.22    );
    6.23  
    6.24 +val literals_ocaml = let
    6.25 +  fun chr i =
    6.26 +    let
    6.27 +      val xs = string_of_int i;
    6.28 +      val ys = replicate_string (3 - length (explode xs)) "0";
    6.29 +    in "\\" ^ ys ^ xs end;
    6.30 +  fun char_ocaml c =
    6.31 +    let
    6.32 +      val i = ord c;
    6.33 +      val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
    6.34 +        then chr i else c
    6.35 +    in s end;
    6.36 +in Literals {
    6.37 +  literal_char = enclose "'" "'" o char_ocaml,
    6.38 +  literal_string = quote o translate_string char_ocaml,
    6.39 +  literal_numeral = fn unbounded => fn k => if k >= 0 then
    6.40 +      if unbounded then
    6.41 +        "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    6.42 +      else string_of_int k
    6.43 +    else
    6.44 +      if unbounded then
    6.45 +        "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
    6.46 +          o string_of_int o op ~) k ^ ")"
    6.47 +      else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
    6.48 +  literal_list = Pretty.enum ";" "[" "]",
    6.49 +  infix_cons = (6, "::")
    6.50 +} end;
    6.51 +
    6.52 +
    6.53  
    6.54  (** SML/OCaml generic part **)
    6.55  
    6.56 @@ -839,7 +878,8 @@
    6.57  (** ML (system language) code for evaluation and instrumentalization **)
    6.58  
    6.59  fun ml_code_of thy = Code_Target.serialize_custom thy
    6.60 -  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME "")));
    6.61 +  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
    6.62 +  literals_sml));
    6.63  
    6.64  
    6.65  (* evaluation *)
    6.66 @@ -935,8 +975,8 @@
    6.67        pr_ocaml_module pr_ocaml_stmt module_name);
    6.68  
    6.69  val setup =
    6.70 -  Code_Target.add_target (target_SML, isar_seri_sml)
    6.71 -  #> Code_Target.add_target (target_OCaml, isar_seri_ocaml)
    6.72 +  Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
    6.73 +  #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
    6.74    #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
    6.75        brackify_infix (1, R) fxy [
    6.76          pr_typ (INFX (1, X)) ty1,

     7.1 --- a/src/Tools/code/code_printer.ML	Fri Aug 29 20:36:08 2008 +0200
     7.2 +++ b/src/Tools/code/code_printer.ML	Mon Sep 01 10:18:37 2008 +0200
     7.3 @@ -59,6 +59,16 @@
     7.4      -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
     7.5      -> thm -> fixity -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
     7.6  
     7.7 +  type literals
     7.8 +  val Literals: { literal_char: string -> string, literal_string: string -> string,
     7.9 +        literal_numeral: bool -> int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    7.10 +    -> literals
    7.11 +  val literal_char: literals -> string -> string
    7.12 +  val literal_string: literals -> string -> string
    7.13 +  val literal_numeral: literals -> bool -> int -> string
    7.14 +  val literal_list: literals -> Pretty.T list -> Pretty.T
    7.15 +  val infix_cons: literals -> int * string
    7.16 +
    7.17    val nerror: thm -> string -> 'a
    7.18  end;
    7.19  
    7.20 @@ -276,4 +286,23 @@
    7.21  
    7.22  val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
    7.23  
    7.24 +
    7.25 +(** pretty literals **)
    7.26 +
    7.27 +datatype literals = Literals of {
    7.28 +  literal_char: string -> string,
    7.29 +  literal_string: string -> string,
    7.30 +  literal_numeral: bool -> int -> string,
    7.31 +  literal_list: Pretty.T list -> Pretty.T,
    7.32 +  infix_cons: int * string
    7.33 +};
    7.34 +
    7.35 +fun dest_Literals (Literals lits) = lits;
    7.36 +
    7.37 +val literal_char = #literal_char o dest_Literals;
    7.38 +val literal_string = #literal_string o dest_Literals;
    7.39 +val literal_numeral = #literal_numeral o dest_Literals;
    7.40 +val literal_list = #literal_list o dest_Literals;
    7.41 +val infix_cons = #infix_cons o dest_Literals;
    7.42 +
    7.43  end; (*struct*)

     8.1 --- a/src/Tools/code/code_target.ML	Fri Aug 29 20:36:08 2008 +0200
     8.2 +++ b/src/Tools/code/code_target.ML	Mon Sep 01 10:18:37 2008 +0200
     8.3 @@ -10,7 +10,7 @@
     8.4    include CODE_PRINTER
     8.5  
     8.6    type serializer
     8.7 -  val add_target: string * serializer -> theory -> theory
     8.8 +  val add_target: string * (serializer * literals) -> theory -> theory
     8.9    val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
    8.10      -> theory -> theory
    8.11    val assert_target: theory -> string -> string
    8.12 @@ -28,7 +28,7 @@
    8.13      -> 'a -> serialization
    8.14    val serialize: theory -> string -> string option -> Args.T list
    8.15      -> Code_Thingol.program -> string list -> serialization
    8.16 -  val serialize_custom: theory -> string * serializer
    8.17 +  val serialize_custom: theory -> string * (serializer * literals)
    8.18      -> Code_Thingol.program -> string list -> string * string list
    8.19    val compile: serialization -> unit
    8.20    val export: serialization -> unit
    8.21 @@ -51,13 +51,13 @@
    8.22      -> (theory -> theory) * OuterParse.token list
    8.23    val add_reserved: string -> string -> theory -> theory
    8.24  
    8.25 -  val add_pretty_list: string -> string -> string -> theory -> theory
    8.26 -  val add_pretty_list_string: string -> string -> string
    8.27 +  val add_literal_list: string -> string -> string -> theory -> theory
    8.28 +  val add_literal_list_string: string -> string -> string
    8.29      -> string -> string list -> theory -> theory
    8.30 -  val add_pretty_char: string -> string -> string list -> theory -> theory
    8.31 -  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
    8.32 +  val add_literal_char: string -> string -> string list -> theory -> theory
    8.33 +  val add_literal_numeral: string -> bool -> bool -> string -> string -> string
    8.34      -> string -> string -> theory -> theory
    8.35 -  val add_pretty_message: string -> string -> string list -> string
    8.36 +  val add_literal_message: string -> string -> string list -> string
    8.37      -> string -> string -> theory -> theory
    8.38  end;
    8.39  
    8.40 @@ -147,67 +147,7 @@
    8.41    in dest_numeral #> the_default 0 end;
    8.42  
    8.43  
    8.44 -(* pretty syntax printing *)
    8.45 -
    8.46 -local
    8.47 -
    8.48 -fun ocaml_char c =
    8.49 -  let
    8.50 -    fun chr i =
    8.51 -      let
    8.52 -        val xs = string_of_int i;
    8.53 -        val ys = replicate_string (3 - length (explode xs)) "0";
    8.54 -      in "\\" ^ ys ^ xs end;
    8.55 -    val i = ord c;
    8.56 -    val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
    8.57 -      then chr i else c
    8.58 -  in s end;
    8.59 -
    8.60 -fun haskell_char c =
    8.61 -  let
    8.62 -    val s = ML_Syntax.print_char c;
    8.63 -  in if s = "'" then "\\'" else s end;
    8.64 -
    8.65 -val pretty : (string * {
    8.66 -    pretty_char: string -> string,
    8.67 -    pretty_string: string -> string,
    8.68 -    pretty_numeral: bool -> int -> string,
    8.69 -    pretty_list: Pretty.T list -> Pretty.T,
    8.70 -    infix_cons: int * string
    8.71 -  }) list = [
    8.72 -  ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
    8.73 -      pretty_string = quote o translate_string ML_Syntax.print_char,
    8.74 -      pretty_numeral = fn unbounded => fn k =>
    8.75 -        if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
    8.76 -        else string_of_int k,
    8.77 -      pretty_list = Pretty.enum "," "[" "]",
    8.78 -      infix_cons = (7, "::")}),
    8.79 -  ("OCaml", { pretty_char = enclose "'" "'" o ocaml_char,
    8.80 -      pretty_string = quote o translate_string ocaml_char,
    8.81 -      pretty_numeral = fn unbounded => fn k => if k >= 0 then
    8.82 -            if unbounded then
    8.83 -              "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    8.84 -            else string_of_int k
    8.85 -          else
    8.86 -            if unbounded then
    8.87 -              "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
    8.88 -                o string_of_int o op ~) k ^ ")"
    8.89 -            else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
    8.90 -      pretty_list = Pretty.enum ";" "[" "]",
    8.91 -      infix_cons = (6, "::")}),
    8.92 -  ("Haskell", { pretty_char = enclose "'" "'" o haskell_char,
    8.93 -      pretty_string = quote o translate_string haskell_char,
    8.94 -      pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
    8.95 -          else enclose "(" ")" (signed_string_of_int k),
    8.96 -      pretty_list = Pretty.enum "," "[" "]",
    8.97 -      infix_cons = (5, ":")})
    8.98 -];
    8.99 -
   8.100 -in
   8.101 -
   8.102 -fun pr_pretty target = case AList.lookup (op =) pretty target
   8.103 - of SOME x => x
   8.104 -  | NONE => error ("Unknown code target language: " ^ quote target);
   8.105 +(* literal syntax printing *)
   8.106  
   8.107  fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   8.108    brackify_infix (target_fxy, R) fxy [
   8.109 @@ -216,51 +156,48 @@
   8.110      pr (INFX (target_fxy, R)) t2
   8.111    ];
   8.112  
   8.113 -fun pretty_list c_nil c_cons target =
   8.114 +fun pretty_list c_nil c_cons literals =
   8.115    let
   8.116 -    val pretty_ops = pr_pretty target;
   8.117 -    val mk_list = #pretty_list pretty_ops;
   8.118 +    val mk_list = literal_list literals;
   8.119      fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
   8.120        case Option.map (cons t1) (implode_list c_nil c_cons t2)
   8.121         of SOME ts => mk_list (map (pr vars NOBR) ts)
   8.122 -        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
   8.123 +        | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
   8.124    in (2, pretty) end;
   8.125  
   8.126 -fun pretty_list_string c_nil c_cons c_char c_nibbles target =
   8.127 +fun pretty_list_string c_nil c_cons c_char c_nibbles literals =
   8.128    let
   8.129 -    val pretty_ops = pr_pretty target;
   8.130 -    val mk_list = #pretty_list pretty_ops;
   8.131 -    val mk_char = #pretty_char pretty_ops;
   8.132 -    val mk_string = #pretty_string pretty_ops;
   8.133 +    val mk_list = literal_list literals;
   8.134 +    val mk_char = literal_char literals;
   8.135 +    val mk_string = literal_string literals;
   8.136      fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
   8.137        case Option.map (cons t1) (implode_list c_nil c_cons t2)
   8.138         of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
   8.139             of SOME p => p
   8.140              | NONE => mk_list (map (pr vars NOBR) ts))
   8.141 -        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
   8.142 +        | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
   8.143    in (2, pretty) end;
   8.144  
   8.145 -fun pretty_char c_char c_nibbles target =
   8.146 +fun pretty_char c_char c_nibbles literals =
   8.147    let
   8.148 -    val mk_char = #pretty_char (pr_pretty target);
   8.149 +    val mk_char = literal_char literals;
   8.150      fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
   8.151        case decode_char c_nibbles (t1, t2)
   8.152         of SOME c => (str o mk_char) c
   8.153          | NONE => nerror thm "Illegal character expression";
   8.154    in (2, pretty) end;
   8.155  
   8.156 -fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
   8.157 +fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 literals =
   8.158    let
   8.159 -    val mk_numeral = #pretty_numeral (pr_pretty target);
   8.160 +    val mk_numeral = literal_numeral literals;
   8.161      fun pretty _ thm _ _ _ [(t, _)] =
   8.162        (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
   8.163    in (1, pretty) end;
   8.164  
   8.165 -fun pretty_message c_char c_nibbles c_nil c_cons target =
   8.166 +fun pretty_message c_char c_nibbles c_nil c_cons literals =
   8.167    let
   8.168 -    val pretty_ops = pr_pretty target;
   8.169 -    val mk_char = #pretty_char pretty_ops;
   8.170 -    val mk_string = #pretty_string pretty_ops;
   8.171 +    val mk_char = literal_char literals;
   8.172 +    val mk_string = literal_string literals;
   8.173      fun pretty _ thm _ _ _ [(t, _)] =
   8.174        case implode_list c_nil c_cons t
   8.175         of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
   8.176 @@ -269,8 +206,6 @@
   8.177          | NONE => nerror thm "Illegal message expression";
   8.178    in (1, pretty) end;
   8.179  
   8.180 -end; (*local*)
   8.181 -
   8.182  
   8.183  (** theory data **)
   8.184  
   8.185 @@ -308,7 +243,7 @@
   8.186    -> string list                        (*selected statements*)
   8.187    -> serialization;
   8.188  
   8.189 -datatype serializer_entry = Serializer of serializer
   8.190 +datatype serializer_entry = Serializer of serializer * literals
   8.191    | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
   8.192  
   8.193  datatype target = Target of {
   8.194 @@ -562,57 +497,67 @@
   8.195  fun add_syntax_constP target c = parse_syntax fst
   8.196    >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
   8.197  
   8.198 -fun add_pretty_list target nill cons thy =
   8.199 +fun the_literals thy =
   8.200 +  let
   8.201 +    val (targets, _) = CodeTargetData.get thy;
   8.202 +    fun literals target = case Symtab.lookup targets target
   8.203 +     of SOME data => (case the_serializer data
   8.204 +         of Serializer (_, literals) => literals
   8.205 +          | Extends (super, _) => literals super)
   8.206 +      | NONE => error ("Unknown code target language: " ^ quote target);
   8.207 +  in literals end;
   8.208 +
   8.209 +fun add_literal_list target nill cons thy =
   8.210    let
   8.211      val nil' = Code_Name.const thy nill;
   8.212      val cons' = Code_Name.const thy cons;
   8.213 -    val pr = pretty_list nil' cons' target;
   8.214 +    val pr = pretty_list nil' cons' (the_literals thy target);
   8.215    in
   8.216      thy
   8.217      |> add_syntax_const target cons (SOME pr)
   8.218    end;
   8.219  
   8.220 -fun add_pretty_list_string target nill cons charr nibbles thy =
   8.221 +fun add_literal_list_string target nill cons charr nibbles thy =
   8.222    let
   8.223      val nil' = Code_Name.const thy nill;
   8.224      val cons' = Code_Name.const thy cons;
   8.225      val charr' = Code_Name.const thy charr;
   8.226      val nibbles' = map (Code_Name.const thy) nibbles;
   8.227 -    val pr = pretty_list_string nil' cons' charr' nibbles' target;
   8.228 +    val pr = pretty_list_string nil' cons' charr' nibbles' (the_literals thy target);
   8.229    in
   8.230      thy
   8.231      |> add_syntax_const target cons (SOME pr)
   8.232    end;
   8.233  
   8.234 -fun add_pretty_char target charr nibbles thy =
   8.235 +fun add_literal_char target charr nibbles thy =
   8.236    let
   8.237      val charr' = Code_Name.const thy charr;
   8.238      val nibbles' = map (Code_Name.const thy) nibbles;
   8.239 -    val pr = pretty_char charr' nibbles' target;
   8.240 +    val pr = pretty_char charr' nibbles' (the_literals thy target);
   8.241    in
   8.242      thy
   8.243      |> add_syntax_const target charr (SOME pr)
   8.244    end;
   8.245  
   8.246 -fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   8.247 +fun add_literal_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   8.248    let
   8.249      val pls' = Code_Name.const thy pls;
   8.250      val min' = Code_Name.const thy min;
   8.251      val bit0' = Code_Name.const thy bit0;
   8.252      val bit1' = Code_Name.const thy bit1;
   8.253 -    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
   8.254 +    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' (the_literals thy target);
   8.255    in
   8.256      thy
   8.257      |> add_syntax_const target number_of (SOME pr)
   8.258    end;
   8.259  
   8.260 -fun add_pretty_message target charr nibbles nill cons str thy =
   8.261 +fun add_literal_message target charr nibbles nill cons str thy =
   8.262    let
   8.263      val charr' = Code_Name.const thy charr;
   8.264      val nibbles' = map (Code_Name.const thy) nibbles;
   8.265      val nil' = Code_Name.const thy nill;
   8.266      val cons' = Code_Name.const thy cons;
   8.267 -    val pr = pretty_message charr' nibbles' nil' cons' target;
   8.268 +    val pr = pretty_message charr' nibbles' nil' cons' (the_literals thy target);
   8.269    in
   8.270      thy
   8.271      |> add_syntax_const target str (SOME pr)
   8.272 @@ -658,7 +603,7 @@
   8.273            in (modify' #> modify, merge_target false target (data', data)) end
   8.274        end;
   8.275      val (modify, data) = collapse_hierarchy target;
   8.276 -    val serializer = the_default (case the_serializer data
   8.277 +    val (serializer, _) = the_default (case the_serializer data
   8.278       of Serializer seri => seri) alt_serializer;
   8.279      val reserved = the_reserved data;
   8.280      val includes = Symtab.dest (the_includes data);