Add :trace and :goto commands to view and move in the current trace

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -29,6 +29,7 @@ import de.prob2.jupyter.commands.ConstantsCommand;
 import de.prob2.jupyter.commands.DotCommand;
 import de.prob2.jupyter.commands.EvalCommand;
 import de.prob2.jupyter.commands.ExecCommand;
+import de.prob2.jupyter.commands.GotoCommand;
 import de.prob2.jupyter.commands.GroovyCommand;
 import de.prob2.jupyter.commands.HelpCommand;
 import de.prob2.jupyter.commands.InitialiseCommand;
@@ -42,6 +43,7 @@ import de.prob2.jupyter.commands.ShowCommand;
 import de.prob2.jupyter.commands.SolveCommand;
 import de.prob2.jupyter.commands.TableCommand;
 import de.prob2.jupyter.commands.TimeCommand;
+import de.prob2.jupyter.commands.TraceCommand;
 import de.prob2.jupyter.commands.TypeCommand;
 import de.prob2.jupyter.commands.VersionCommand;
 
@@ -150,9 +152,11 @@ public final class ProBKernel extends BaseKernel {
 		this.commands.put("::load", injector.getInstance(LoadCellCommand.class));
 		this.commands.put(":pref", injector.getInstance(PrefCommand.class));
 		this.commands.put(":browse", injector.getInstance(BrowseCommand.class));
+		this.commands.put(":trace", injector.getInstance(TraceCommand.class));
 		this.commands.put(":exec", injector.getInstance(ExecCommand.class));
 		this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
 		this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
+		this.commands.put(":goto", injector.getInstance(GotoCommand.class));
 		this.commands.put(":show", injector.getInstance(ShowCommand.class));
 		this.commands.put(":dot", injector.getInstance(DotCommand.class));
 		this.commands.put(":assert", injector.getInstance(AssertCommand.class));

src/main/java/de/prob2/jupyter/commands/GotoCommand.java

+package de.prob2.jupyter.commands;
+
+import com.google.inject.Inject;
+
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class GotoCommand implements Command {
+	private final @NotNull AnimationSelector animationSelector;
+	
+	@Inject
+	private GotoCommand(final @NotNull AnimationSelector animationSelector) {
+		super();
+		
+		this.animationSelector = animationSelector;
+	}
+	
+	@Override
+	public @NotNull String getSyntax() {
+		return ":goto INDEX";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Go to the state with the specified index in the current trace.";
+	}
+	
+	@Override
+	public @NotNull String getHelpBody() {
+		return "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n\nGoing backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition).";
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		final int index = Integer.parseInt(argString);
+		final Trace trace = this.animationSelector.getCurrentTrace();
+		if (index < -1 || index >= trace.size()) {
+			throw new UserErrorException(String.format("Invalid trace index %d, must be in -1..%d", index, trace.size()-1));
+		}
+		this.animationSelector.changeCurrentAnimation(trace.gotoPosition(index));
+		return new DisplayData("Changed to state with index " + index);
+	}
+	
+	@Override
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+		return null;
+	}
+}

src/main/java/de/prob2/jupyter/commands/TraceCommand.java

+package de.prob2.jupyter.commands;
+
+import java.util.List;
+
+import com.google.inject.Inject;
+
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+import de.prob.statespace.Transition;
+
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class TraceCommand implements Command {
+	private final @NotNull AnimationSelector animationSelector;
+	
+	@Inject
+	private TraceCommand(final @NotNull AnimationSelector animationSelector) {
+		super();
+		
+		this.animationSelector = animationSelector;
+	}
+	
+	@Override
+	public @NotNull String getSyntax() {
+		return ":trace";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Display all states and transitions in the current trace.";
+	}
+	
+	@Override
+	public @NotNull String getHelpBody() {
+		return "Each state has an index, which can be passed to the `:goto` command to go to that state.\n\nThe first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.";
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		if (!argString.isEmpty()) {
+			throw new UserErrorException("Expected no arguments");
+		}
+		
+		final Trace trace = this.animationSelector.getCurrentTrace();
+		final StringBuilder sbPlain = new StringBuilder("-1: Root state");
+		final StringBuilder sbMarkdown = new StringBuilder("* -1: Root state");
+		
+		if (trace.getCurrent().getIndex() == -1) {
+			sbPlain.append(" (current)");
+			sbMarkdown.append(" **(current)**");
+		}
+		
+		final List<Transition> transitionList = trace.getTransitionList();
+		for (int i = 0; i < transitionList.size(); i++) {
+			final Transition transition = transitionList.get(i);
+			sbPlain.append('\n');
+			sbPlain.append(i);
+			sbPlain.append(": ");
+			sbPlain.append(transition);
+			sbMarkdown.append("\n* ");
+			sbMarkdown.append(i);
+			sbMarkdown.append(": ");
+			sbMarkdown.append(transition);
+			
+			if (trace.getCurrent().getIndex() == i) {
+				sbPlain.append(" (current)");
+				sbMarkdown.append(" **(current)**");
+			}
+		}
+		
+		final DisplayData result = new DisplayData(sbPlain.toString());
+		result.putMarkdown(sbMarkdown.toString());
+		return result;
+	}
+	
+	@Override
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+		return null;
+	}
+}