(String value)
| 741 | } |
| 742 | |
| 743 | private void string(String value) throws IOException { |
| 744 | String[] replacements = htmlSafe ? HTML_SAFE_REPLACEMENT_CHARS : REPLACEMENT_CHARS; |
| 745 | out.write('\"'); |
| 746 | int last = 0; |
| 747 | int length = value.length(); |
| 748 | for (int i = 0; i < length; i++) { |
| 749 | char c = value.charAt(i); |
| 750 | String replacement; |
| 751 | if (c < 128) { |
| 752 | replacement = replacements[c]; |
| 753 | if (replacement == null) { |
| 754 | continue; |
| 755 | } |
| 756 | } else if (c == '\u2028') { |
| 757 | replacement = "\\u2028"; |
| 758 | } else if (c == '\u2029') { |
| 759 | replacement = "\\u2029"; |
| 760 | } else { |
| 761 | continue; |
| 762 | } |
| 763 | if (last < i) { |
| 764 | out.write(value, last, i - last); |
| 765 | } |
| 766 | out.write(replacement); |
| 767 | last = i + 1; |
| 768 | } |
| 769 | if (last < length) { |
| 770 | out.write(value, last, length - last); |
| 771 | } |
| 772 | out.write('\"'); |
| 773 | } |
| 774 | |
| 775 | private void newline() throws IOException { |
| 776 | if (usesEmptyNewlineAndIndent) { |
no test coverage detected