Looking at the following terminal output (using the WebIDE):

>'\x00'
="\x00"
>'\x19'
="\x19"
>'\x20'
=" "
>'\x7F'
="�"
>'\xFF'
="ÿ"
> 

You can see that characters from 0x00 - 0x19 are correctly escaped but values from 0x7F to 0xFF are not, although these should be considered non-printable or non-ascii

This has adverse effects on things like dump(); that send non-printable/non-ascii values to the console.

A simple change on a single line should fix it.

49.    if (ch<32) {

becomes

49.    if (ch<32 || ch>=127) {