From b2ea07d87189e7f45b7316a91c8e3e36d899a0e4 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 2 Jul 2018 14:05:44 +0200
Subject: [PATCH] Add :trace and :goto commands to view and move in the current
 trace

---
 .../java/de/prob2/jupyter/ProBKernel.java     |  4 +
 .../prob2/jupyter/commands/GotoCommand.java   | 56 ++++++++++++
 .../prob2/jupyter/commands/TraceCommand.java  | 86 +++++++++++++++++++
 3 files changed, 146 insertions(+)
 create mode 100644 src/main/java/de/prob2/jupyter/commands/GotoCommand.java
 create mode 100644 src/main/java/de/prob2/jupyter/commands/TraceCommand.java

diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 9204812..04add0d 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/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));
diff --git a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
new file mode 100644
index 0000000..37f8d86
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
@@ -0,0 +1,56 @@
+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;
+	}
+}
diff --git a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
new file mode 100644
index 0000000..72ff13f
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
@@ -0,0 +1,86 @@
+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;
+	}
+}
-- 
GitLab