# HG changeset patch
# User berghofe
# Date 1175071639 -7200
# Node ID ad3bd3d6ba8a1147837b020329ea98b448a2c54a
# Parent  3ccb92dfb5e933459813edae65fa1845b0c980a8
Improved code generator for characters: now handles
non-printable characters as well.

diff -r 3ccb92dfb5e9 -r ad3bd3d6ba8a src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 28 01:55:18 2007 +0200
+++ b/src/HOL/List.thy	Wed Mar 28 10:47:19 2007 +0200
@@ -2710,11 +2710,8 @@
   in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
 fun char_codegen thy defs gr dep thyname b t =
-  case (Option.map chr o try HOLogic.dest_char) t 
-   of SOME c =>
-        if Symbol.is_printable c
-        then SOME (gr, (Pretty.quote o Pretty.str) c)
-        else NONE
+  case Option.map chr (try HOLogic.dest_char t) of
+      SOME c => SOME (gr, Pretty.quote (Pretty.str (ML_Syntax.print_char c)))
     | NONE => NONE;
 
 in