Skip to content
Snippets Groups Projects
Commit a77c9859 authored by dgelessus's avatar dgelessus
Browse files

Update ShowCommand to match API changes in ProB 2

parent 856f768e
No related branches found
No related tags found
No related merge requests found
...@@ -8,6 +8,7 @@ import com.google.inject.Inject; ...@@ -8,6 +8,7 @@ import com.google.inject.Inject;
import de.prob.animator.command.GetAnimationMatrixForStateCommand; import de.prob.animator.command.GetAnimationMatrixForStateCommand;
import de.prob.animator.command.GetImagesForMachineCommand; import de.prob.animator.command.GetImagesForMachineCommand;
import de.prob.animator.command.GetPreferenceCommand; import de.prob.animator.command.GetPreferenceCommand;
import de.prob.animator.domainobjects.AnimationMatrixEntry;
import de.prob.statespace.AnimationSelector; import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace; import de.prob.statespace.Trace;
...@@ -94,20 +95,21 @@ public final class ShowCommand implements Command { ...@@ -94,20 +95,21 @@ public final class ShowCommand implements Command {
tableBuilder.append("px"); tableBuilder.append("px");
} }
tableBuilder.append("\"><tbody>"); tableBuilder.append("\"><tbody>");
for (final List<Object> row : cmdMatrix.getMatrix()) { for (final List<AnimationMatrixEntry> row : cmdMatrix.getMatrix()) {
tableBuilder.append("\n<tr>"); tableBuilder.append("\n<tr>");
for (final Object entry : row) { for (final AnimationMatrixEntry entry : row) {
final int padding; final int padding;
final String contents; final String contents;
if (entry == null) { if (entry == null) {
padding = 0; padding = 0;
contents = ""; contents = "";
} else if (entry instanceof Integer) { } else if (entry instanceof AnimationMatrixEntry.Image) {
final AnimationMatrixEntry.Image imageEntry = (AnimationMatrixEntry.Image)entry;
padding = imagePadding; padding = imagePadding;
contents = String.format("<img alt=\"%d\" src=\"%s\"/>", entry, images.get(entry)); contents = String.format("<img alt=\"%d\" src=\"%s\"/>", imageEntry.getImageNumber(), images.get(imageEntry.getImageNumber()));
} else if (entry instanceof String) { } else if (entry instanceof AnimationMatrixEntry.Text) {
padding = stringPadding; padding = stringPadding;
contents = (String)entry; contents = ((AnimationMatrixEntry.Text)entry).getText();
} else { } else {
throw new AssertionError("Unhandled animation matrix entry type: " + entry.getClass()); throw new AssertionError("Unhandled animation matrix entry type: " + entry.getClass());
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment