public final void displayForeignStringAsLiteral(byte[] s, PrintStream port) {
        try {
            StringBuilder sb = new StringBuilder();
            sb.append('"');
            for (int i = 0; i < s.length; i++) {
                char c = decode(s[i]);
                if (c >= 0x20 && c <= 0x7E) {
                    if (c == '"' || c == '\\') {
                        sb.append('\\');
                    }
                    sb.append(c);
                } else {
                    sb.append("\\x");
                    sb.append(Hex.b(s[i]));
                }
            }
            sb.append('"');
            port.write(sb.toString().getBytes("utf-8"));
        } catch (UnsupportedEncodingException e) {
            throw new RuntimeException("utf-8 is an Unsupported Encoding?  In Java???", e);
        } catch (IOException e) {
            throw new RuntimeException("I/O error", e);
        }
    }