From a9b592ec264199011499357bafbcb7ba542ef99b Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Thu, 28 Jun 2018 13:23:03 +0200 Subject: [PATCH] Support style preferences in :show --- notebooks/tests/show.ipynb | 389 ++++++++++++++---- .../prob2/jupyter/commands/ShowCommand.java | 58 ++- 2 files changed, 358 insertions(+), 89 deletions(-) diff --git a/notebooks/tests/show.ipynb b/notebooks/tests/show.ipynb index 9ee27a2..2c29599 100644 --- a/notebooks/tests/show.ipynb +++ b/notebooks/tests/show.ipynb @@ -139,31 +139,31 @@ { "data": { "text/markdown": [ - "<table><tbody>\n", + "<table style=\"font-family:monospace\"><tbody>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "</tbody></table>" ], @@ -208,31 +208,31 @@ { "data": { "text/markdown": [ - "<table><tbody>\n", + "<table style=\"font-family:monospace\"><tbody>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "</tbody></table>" ], @@ -277,31 +277,31 @@ { "data": { "text/markdown": [ - "<table><tbody>\n", + "<table style=\"font-family:monospace\"><tbody>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", - "<td style=\"padding:0\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", "</tr>\n", "</tbody></table>" ], @@ -322,7 +322,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Text labels are supported." + "The image padding preference is respected." ] }, { @@ -333,7 +333,7 @@ { "data": { "text/plain": [ - "Loaded machine: CrosswordPuzzle : []\n" + "Preference changed: TK_CUSTOM_STATE_VIEW_PADDING = 8\n" ] }, "execution_count": 12, @@ -342,7 +342,7 @@ } ], "source": [ - ":load CrosswordPuzzle.mch" + ":pref TK_CUSTOM_STATE_VIEW_PADDING=8" ] }, { @@ -352,8 +352,37 @@ "outputs": [ { "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "<td style=\"padding:8px\"></td>\n", + "</tr>\n", + "</tbody></table>" + ], "text/plain": [ - "Machine constants set up using operation 0: $setup_constants()" + "<Animation function visualisation>" ] }, "execution_count": 13, @@ -362,7 +391,14 @@ } ], "source": [ - ":constants" + ":show" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Text labels are supported." ] }, { @@ -373,7 +409,7 @@ { "data": { "text/plain": [ - "Machine initialised using operation 1: $initialise_machine()" + "Loaded machine: CrosswordPuzzle : []\n" ] }, "execution_count": 14, @@ -382,45 +418,85 @@ } ], "source": [ - ":init" + ":load CrosswordPuzzle.mch" ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine constants set up using operation 0: $setup_constants()" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":constants" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine initialised using operation 1: $initialise_machine()" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "<table><tbody>\n", + "<table style=\"font-family:monospace\"><tbody>\n", "<tr>\n", - "<td style=\"padding:0\">S</td>\n", - "<td style=\"padding:0\">T</td>\n", - "<td style=\"padding:0\">E</td>\n", - "<td style=\"padding:0\">E</td>\n", - "<td style=\"padding:0\">R</td>\n", + "<td style=\"padding:10px\">S</td>\n", + "<td style=\"padding:10px\">T</td>\n", + "<td style=\"padding:10px\">E</td>\n", + "<td style=\"padding:10px\">E</td>\n", + "<td style=\"padding:10px\">R</td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\">-</td>\n", - "<td style=\"padding:0\">-</td>\n", - "<td style=\"padding:0\">A</td>\n", - "<td style=\"padding:0\">-</td>\n", - "<td style=\"padding:0\">U</td>\n", + "<td style=\"padding:10px\">-</td>\n", + "<td style=\"padding:10px\">-</td>\n", + "<td style=\"padding:10px\">A</td>\n", + "<td style=\"padding:10px\">-</td>\n", + "<td style=\"padding:10px\">U</td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\">-</td>\n", - "<td style=\"padding:0\">I</td>\n", - "<td style=\"padding:0\">R</td>\n", - "<td style=\"padding:0\">O</td>\n", - "<td style=\"padding:0\">N</td>\n", + "<td style=\"padding:10px\">-</td>\n", + "<td style=\"padding:10px\">I</td>\n", + "<td style=\"padding:10px\">R</td>\n", + "<td style=\"padding:10px\">O</td>\n", + "<td style=\"padding:10px\">N</td>\n", "</tr>\n", "<tr>\n", - "<td style=\"padding:0\">-</td>\n", - "<td style=\"padding:0\">-</td>\n", - "<td style=\"padding:0\">N</td>\n", - "<td style=\"padding:0\">O</td>\n", - "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:10px\">-</td>\n", + "<td style=\"padding:10px\">-</td>\n", + "<td style=\"padding:10px\">N</td>\n", + "<td style=\"padding:10px\">O</td>\n", + "<td style=\"padding:10px\">-</td>\n", "</tr>\n", "</tbody></table>" ], @@ -428,7 +504,166 @@ "<Animation function visualisation>" ] }, - "execution_count": 15, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The text padding preference is respected." + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: TK_CUSTOM_STATE_VIEW_STRING_PADDING = 2\n" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref TK_CUSTOM_STATE_VIEW_STRING_PADDING=2" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:2px\">S</td>\n", + "<td style=\"padding:2px\">T</td>\n", + "<td style=\"padding:2px\">E</td>\n", + "<td style=\"padding:2px\">E</td>\n", + "<td style=\"padding:2px\">R</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">A</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">U</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">I</td>\n", + "<td style=\"padding:2px\">R</td>\n", + "<td style=\"padding:2px\">O</td>\n", + "<td style=\"padding:2px\">N</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">N</td>\n", + "<td style=\"padding:2px\">O</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The font name and size preferences are supported." + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: TK_CUSTOM_STATE_VIEW_FONT_SIZE = 18\n", + "Preference changed: TK_CUSTOM_STATE_VIEW_FONT_NAME = Arial\n" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref TK_CUSTOM_STATE_VIEW_FONT_NAME=Arial TK_CUSTOM_STATE_VIEW_FONT_SIZE=18" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:\"Arial\" monospace;font-size:18px\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:2px\">S</td>\n", + "<td style=\"padding:2px\">T</td>\n", + "<td style=\"padding:2px\">E</td>\n", + "<td style=\"padding:2px\">E</td>\n", + "<td style=\"padding:2px\">R</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">A</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">U</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">I</td>\n", + "<td style=\"padding:2px\">R</td>\n", + "<td style=\"padding:2px\">O</td>\n", + "<td style=\"padding:2px\">N</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "<td style=\"padding:2px\">N</td>\n", + "<td style=\"padding:2px\">O</td>\n", + "<td style=\"padding:2px\">-</td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java index 16db172..7f71ce1 100644 --- a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java @@ -7,6 +7,7 @@ import com.google.inject.Inject; import de.prob.animator.command.GetAnimationMatrixForStateCommand; import de.prob.animator.command.GetImagesForMachineCommand; +import de.prob.animator.command.GetPreferenceCommand; import de.prob.statespace.AnimationSelector; import de.prob.statespace.Trace; @@ -55,29 +56,62 @@ public final class ShowCommand implements Command { throw new UserErrorException("Machine is not initialised, cannot show animation function visualisation"); } - final GetImagesForMachineCommand cmd1 = new GetImagesForMachineCommand(); - trace.getStateSpace().execute(cmd1); - final Map<Integer, String> images = cmd1.getImages(); + final GetImagesForMachineCommand cmdImages = new GetImagesForMachineCommand(); + final GetAnimationMatrixForStateCommand cmdMatrix = new GetAnimationMatrixForStateCommand(trace.getCurrentState()); + final GetPreferenceCommand cmdImagePadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_PADDING"); + final GetPreferenceCommand cmdStringPadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_STRING_PADDING"); + final GetPreferenceCommand cmdFontName = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_NAME"); + final GetPreferenceCommand cmdFontSize = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_SIZE"); + trace.getStateSpace().execute( + cmdImages, + cmdMatrix, + cmdImagePadding, + cmdStringPadding, + cmdFontName, + cmdFontSize + ); - final GetAnimationMatrixForStateCommand cmd2 = new GetAnimationMatrixForStateCommand(trace.getCurrentState()); - trace.getStateSpace().execute(cmd2); - - if (cmd2.getMatrix() == null) { + if (cmdMatrix.getMatrix() == null) { throw new UserErrorException("No animation function visualisation available"); } - final StringBuilder tableBuilder = new StringBuilder("<table><tbody>"); - for (final List<Object> row : cmd2.getMatrix()) { + final Map<Integer, String> images = cmdImages.getImages(); + final int imagePadding = Integer.parseInt(cmdImagePadding.getValue()); + final int stringPadding = Integer.parseInt(cmdStringPadding.getValue()); + final String fontName = cmdFontName.getValue(); + final int fontSize = Integer.parseInt(cmdFontSize.getValue()); + + final StringBuilder tableBuilder = new StringBuilder("<table style=\"font-family:"); + if (!fontName.isEmpty()) { + tableBuilder.append('"'); + tableBuilder.append(fontName); + tableBuilder.append("\" "); + } + tableBuilder.append("monospace"); + if (fontSize != 0) { + tableBuilder.append(";font-size:"); + tableBuilder.append(fontSize); + tableBuilder.append("px"); + } + tableBuilder.append("\"><tbody>"); + for (final List<Object> row : cmdMatrix.getMatrix()) { tableBuilder.append("\n<tr>"); for (final Object entry : row) { - tableBuilder.append("\n<td style=\"padding:0\">"); + final int padding; + final String contents; if (entry instanceof Integer) { - tableBuilder.append(String.format("", entry, images.get(entry))); + padding = imagePadding; + contents = String.format("", entry, images.get(entry)); } else if (entry instanceof String) { - tableBuilder.append(entry); + padding = stringPadding; + contents = (String)entry; } else { throw new AssertionError("Unhandled animation matrix entry type: " + entry.getClass()); } + tableBuilder.append("\n<td style=\"padding:"); + tableBuilder.append(padding); + tableBuilder.append("px\">"); + tableBuilder.append(contents); tableBuilder.append("</td>"); } tableBuilder.append("\n</tr>"); -- GitLab