diff -r 84bab99dda50 -r 8e38caf43ca8 java/sql-dk/src/info/globalcode/sql/dk/Functions.java --- a/java/sql-dk/src/info/globalcode/sql/dk/Functions.java Sat Aug 15 14:40:48 2015 +0200 +++ b/java/sql-dk/src/info/globalcode/sql/dk/Functions.java Sat Aug 15 16:12:06 2015 +0200 @@ -24,14 +24,14 @@ import java.io.InputStream; import java.io.InputStreamReader; import java.io.PrintWriter; -import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; import java.util.Collections; -import java.util.Deque; import java.util.List; import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; /** * @@ -39,6 +39,9 @@ */ public class Functions { + private static final String NBSP = " "; + private static final Pattern WHITESPACE_TO_REPLACE = Pattern.compile("\\n|\\r|\\t|" + NBSP); + private Functions() { } @@ -185,4 +188,53 @@ return hierarchy; } + + /** + * TODO: support background or styles and move to ColorfulPrintWriter + * + * @param out + * @param valueString + * @param basicColor + * @param escapeColor + */ + public static void printValueWithWhitespaceReplaced(ColorfulPrintWriter out, String valueString, ColorfulPrintWriter.TerminalColor basicColor, ColorfulPrintWriter.TerminalColor escapeColor) { + + Matcher m = WHITESPACE_TO_REPLACE.matcher(valueString); + + int start = 0; + + while (m.find(start)) { + + printColorOrNot(out, basicColor, valueString.substring(start, m.start())); + + switch (m.group()) { + case "\n": + out.print(escapeColor, "↲"); + break; + case "\r": + out.print(escapeColor, "⏎"); + break; + case "\t": + out.print(escapeColor, "↹"); + break; + case NBSP: + out.print(escapeColor, "⎵"); + break; + default: + throw new IllegalStateException("Unexpected whitespace token: „" + m.group() + "“"); + } + + start = m.end(); + } + + printColorOrNot(out, basicColor, valueString.substring(start, valueString.length())); + } + + private static void printColorOrNot(ColorfulPrintWriter out, ColorfulPrintWriter.TerminalColor color, String text) { + if (color == null) { + out.print(text); + } else { + out.print(color, text); + } + } }