diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb index 8846808e49454b893c7db94bd82c4bbf131258dc..01c6e83f4ce2a9ce0b4f2665abc34207b729742f 100644 --- a/notebooks/tests/pref.ipynb +++ b/notebooks/tests/pref.ipynb @@ -67,6 +67,7 @@ "ALLOY_STRICT_INTEGERS = true\n", "ALLOY_TRANSLATION_FOR_PROOF = false\n", "ALLOY_USE_IMPLEMENTABLE_INTEGERS = false\n", + "ASSERT_CHECKING = true\n", "ATELIERB_KRT_PATH = krt\n", "BBRESULTS = false\n", "BOOL_AS_PREDICATE = false\n", @@ -99,6 +100,7 @@ "DOT_DEFINITIONS_USE_SUB_GRAPH = true\n", "DOT_EDGE_FONT_SIZE = 12\n", "DOT_EDGE_LABELS = true\n", + "DOT_EDGE_PEN_WIDTH = 1\n", "DOT_ENGINE = dot\n", "DOT_EVENT_HIERARCHY_EDGE_COL = #806040\n", "DOT_EVENT_HIERARCHY_EXTENDS_COL = gray50\n", @@ -114,8 +116,10 @@ "DOT_EXPRESSION_NODE_SHAPE = record\n", "DOT_FILL_NORMAL_NODES = false\n", "DOT_FUNCTIONS = false\n", + "DOT_HORIZONTAL_LAYOUT = false\n", "DOT_IDS = false\n", "DOT_INFO = true\n", + "DOT_LIMIT_PAGE_SIZE = true\n", "DOT_LOOPS = true\n", "DOT_MACHINE_HIERARCHY_MAX_IDS = 0\n", "DOT_NODE_FONT_SIZE = 12\n", diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java index c0c4f1347336bac89a0a835353014a63fe0dbb03..320d17fc8f50d3f280a4f50bbd348cf67073c7db 100644 --- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java @@ -1,16 +1,12 @@ package de.prob2.jupyter.commands; -import java.util.ArrayList; import java.util.Collections; import java.util.List; +import java.util.Map; import java.util.TreeMap; import com.google.inject.Inject; -import de.prob.animator.command.ComposedCommand; -import de.prob.animator.command.GetCurrentPreferencesCommand; -import de.prob.animator.command.GetPreferenceCommand; -import de.prob.animator.command.SetPreferenceCommand; import de.prob.statespace.AnimationSelector; import de.prob2.jupyter.Command; import de.prob2.jupyter.CommandUtils; @@ -67,10 +63,9 @@ public final class PrefCommand implements Command { public @NotNull DisplayData run(final @NotNull ParsedArguments args) { final StringBuilder sb = new StringBuilder(); if (args.get(PREFS_PARAM).isEmpty()) { - final GetCurrentPreferencesCommand cmd = new GetCurrentPreferencesCommand(); - this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd); + final Map<String, String> preferences = this.animationSelector.getCurrentTrace().getStateSpace().getCurrentPreferences(); // TreeMap is used to sort the preferences by name. - new TreeMap<>(cmd.getPreferences()).forEach((k, v) -> { + new TreeMap<>(preferences).forEach((k, v) -> { sb.append(k); sb.append(" = "); sb.append(v); @@ -79,29 +74,23 @@ public final class PrefCommand implements Command { } else { final List<String> prefsSplit = args.get(PREFS_PARAM); if (prefsSplit.get(0).contains("=")) { - final List<SetPreferenceCommand> cmds = new ArrayList<>(); - CommandUtils.parsePreferences(prefsSplit).forEach((pref, value) -> { - cmds.add(new SetPreferenceCommand(pref, value)); + final Map<String, String> newPreferenceValues = CommandUtils.parsePreferences(prefsSplit); + this.animationSelector.getCurrentTrace().getStateSpace().changePreferences(newPreferenceValues); + newPreferenceValues.forEach((pref, value) -> { sb.append("Preference changed: "); sb.append(pref); sb.append(" = "); sb.append(value); sb.append('\n'); }); - this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds)); } else { - final List<GetPreferenceCommand> cmds = new ArrayList<>(); for (final String arg : prefsSplit) { if (arg.contains("=")) { throw new UserErrorException(String.format("Cannot view and change preferences in the same command (attempted to assign preference %s)", arg)); } - cmds.add(new GetPreferenceCommand(arg)); - } - this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds)); - for (final GetPreferenceCommand cmd : cmds) { - sb.append(cmd.getKey()); + sb.append(arg); sb.append(" = "); - sb.append(cmd.getValue()); + sb.append(this.animationSelector.getCurrentTrace().getStateSpace().getCurrentPreference(arg)); sb.append('\n'); } }