From 6ea19acdaca0baa3ac9f3da8b6f09562076e0053 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 25 Jun 2018 14:54:37 +0200
Subject: [PATCH] Replace kernel parameter of Command methods with injection

ProBKernel is now a singleton (it's very unlikely that we'll ever need
to run multiple kernels in a single process, and if we do, each would
have its own injector anyway). This allows injecting it into commands
when they need it. This makes more sense than using a parameter,
because most commands don't need access to the kernel object.

We have to use an Injector and inject the kernel only when it's
actually used. We can't inject the kernel as a constructor parameter,
because the ProBKernel constructor injects all the commands, which
would cause a circular dependency.
---
 .../java/de/prob2/jupyter/ProBKernel.java     | 10 ++++++----
 .../prob2/jupyter/commands/AssertCommand.java |  5 ++---
 .../prob2/jupyter/commands/BrowseCommand.java |  5 ++---
 .../de/prob2/jupyter/commands/Command.java    |  6 ++----
 .../jupyter/commands/ConstantsCommand.java    |  5 ++---
 .../de/prob2/jupyter/commands/DotCommand.java |  5 ++---
 .../prob2/jupyter/commands/EvalCommand.java   |  6 ++----
 .../prob2/jupyter/commands/ExecCommand.java   |  5 ++---
 .../prob2/jupyter/commands/GroovyCommand.java | 11 ++++++----
 .../prob2/jupyter/commands/HelpCommand.java   | 20 +++++++++++++++----
 .../jupyter/commands/InitialiseCommand.java   |  5 ++---
 .../jupyter/commands/LoadCellCommand.java     |  5 ++---
 .../jupyter/commands/LoadFileCommand.java     |  5 ++---
 .../prob2/jupyter/commands/PrefCommand.java   |  5 ++---
 .../jupyter/commands/PrettyPrintCommand.java  |  6 ++----
 .../prob2/jupyter/commands/RenderCommand.java |  5 ++---
 .../prob2/jupyter/commands/ShowCommand.java   |  5 ++---
 .../prob2/jupyter/commands/SolveCommand.java  |  5 ++---
 .../prob2/jupyter/commands/TableCommand.java  |  6 ++----
 .../prob2/jupyter/commands/TimeCommand.java   | 14 +++++++++----
 .../prob2/jupyter/commands/TypeCommand.java   |  6 ++----
 .../jupyter/commands/VersionCommand.java      |  6 ++----
 22 files changed, 75 insertions(+), 76 deletions(-)

diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index e51914f..9fdb4e7 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -12,6 +12,7 @@ import java.util.stream.Collectors;
 
 import com.google.inject.Inject;
 import com.google.inject.Injector;
+import com.google.inject.Singleton;
 
 import de.prob.animator.domainobjects.ErrorItem;
 import de.prob.exception.ProBError;
@@ -56,6 +57,7 @@ import org.jetbrains.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+@Singleton
 public final class ProBKernel extends BaseKernel {
 	private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(ProBKernel.class);
 	
@@ -196,7 +198,7 @@ public final class ProBKernel extends BaseKernel {
 		}
 		final DisplayData result;
 		try {
-			result = command.run(this, argString);
+			result = command.run(argString);
 		} catch (final UserErrorException e) {
 			throw new CommandExecutionException(name, e);
 		}
@@ -248,7 +250,7 @@ public final class ProBKernel extends BaseKernel {
 				assert name != null;
 				final String argString = commandMatcher.group(2) == null ? "" : commandMatcher.group(2);
 				if (this.getCommands().containsKey(name)) {
-					final ReplacementOptions replacements = this.getCommands().get(name).complete(this, argString, at - argOffset);
+					final ReplacementOptions replacements = this.getCommands().get(name).complete(argString, at - argOffset);
 					return replacements == null ? null : CommandUtils.offsetReplacementOptions(replacements, argOffset);
 				} else {
 					// Invalid command, can't provide any completions.
@@ -258,7 +260,7 @@ public final class ProBKernel extends BaseKernel {
 		} else if (SPACE_PATTERN.matcher(code).matches()) {
 			// The code contains only whitespace, provide completions from :eval and for command names.
 			final List<String> replacementStrings = new ArrayList<>();
-			final ReplacementOptions evalReplacements = this.getCommands().get(":eval").complete(this, code, at);
+			final ReplacementOptions evalReplacements = this.getCommands().get(":eval").complete(code, at);
 			if (evalReplacements != null) {
 				replacementStrings.addAll(evalReplacements.getReplacements());
 			}
@@ -266,7 +268,7 @@ public final class ProBKernel extends BaseKernel {
 			return new ReplacementOptions(replacementStrings, at, at);
 		} else {
 			// The code is not a valid command, ask :eval for completions.
-			return this.getCommands().get(":eval").complete(this, code, at);
+			return this.getCommands().get(":eval").complete(code, at);
 		}
 	}
 	
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 7c31117..ab8cfc0 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -7,7 +7,6 @@ import de.prob.animator.domainobjects.EvalResult;
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -37,7 +36,7 @@ public final class AssertCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final AbstractEvalResult result = this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE);
 		if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
 			// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
@@ -54,7 +53,7 @@ public final class AssertCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index 050c1df..df7eeec 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -17,7 +17,6 @@ import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -58,7 +57,7 @@ public final class BrowseCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		if (!argString.isEmpty()) {
 			throw new UserErrorException("Unexpected argument: " + argString);
 		}
@@ -90,7 +89,7 @@ public final class BrowseCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return null;
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/Command.java b/src/main/java/de/prob2/jupyter/commands/Command.java
index 5f30dd6..7c7f5a3 100644
--- a/src/main/java/de/prob2/jupyter/commands/Command.java
+++ b/src/main/java/de/prob2/jupyter/commands/Command.java
@@ -1,7 +1,5 @@
 package de.prob2.jupyter.commands;
 
-import de.prob2.jupyter.ProBKernel;
-
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -13,7 +11,7 @@ public interface Command {
 	
 	public abstract @NotNull String getShortHelp();
 	
-	public abstract @Nullable DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString);
+	public abstract @Nullable DisplayData run(final @NotNull String argString);
 	
-	public abstract @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at);
+	public abstract @Nullable ReplacementOptions complete(final @NotNull String argString, final int at);
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 2535c0d..ca25502 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -10,7 +10,6 @@ import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -39,7 +38,7 @@ public final class ConstantsCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString);
 		final Transition op = trace.getCurrentState().findTransition("$setup_constants", predicates);
@@ -58,7 +57,7 @@ public final class ConstantsCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index 6d8d556..54fc9e5 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -20,7 +20,6 @@ import de.prob.animator.domainobjects.IEvalElement;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -49,7 +48,7 @@ public final class DotCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final List<String> split = CommandUtils.splitArgs(argString, 2);
 		assert !split.isEmpty();
 		final String command = split.get(0);
@@ -88,7 +87,7 @@ public final class DotCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final int cmdNameEnd;
 		final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
 		if (argSplitMatcher.find()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index 4b915f5..87d426b 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -5,8 +5,6 @@ import com.google.inject.Inject;
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
 
-import de.prob2.jupyter.ProBKernel;
-
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -33,12 +31,12 @@ public final class EvalCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		return CommandUtils.displayDataForEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.EXPAND));
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 31774a1..c74e114 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -14,7 +14,6 @@ import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -43,7 +42,7 @@ public final class ExecCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final List<String> split = CommandUtils.splitArgs(argString, 2);
 		assert !split.isEmpty();
 		final String opNameOrId = split.get(0);
@@ -74,7 +73,7 @@ public final class ExecCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final int opNameEnd;
 		final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
 		if (argSplitMatcher.find()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
index 3d28c1a..b665132 100644
--- a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
@@ -6,6 +6,7 @@ import javax.script.ScriptEngine;
 import javax.script.ScriptException;
 
 import com.google.inject.Inject;
+import com.google.inject.Injector;
 
 import de.prob.scripting.ScriptEngineProvider;
 
@@ -18,12 +19,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class GroovyCommand implements Command {
+	private final @NotNull Injector injector;
 	private final @NotNull ScriptEngine groovyScriptEngine;
 	
 	@Inject
-	private GroovyCommand(final @NotNull ScriptEngineProvider scriptEngineProvider) {
+	private GroovyCommand(final @NotNull Injector injector, final @NotNull ScriptEngineProvider scriptEngineProvider) {
 		super();
 		
+		this.injector = injector;
 		this.groovyScriptEngine = scriptEngineProvider.get();
 	}
 	
@@ -38,8 +41,8 @@ public final class GroovyCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
-		this.groovyScriptEngine.put("__console", kernel.getIO().out);
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		this.groovyScriptEngine.put("__console", this.injector.getInstance(ProBKernel.class).getIO().out);
 		final Object result;
 		try {
 			result = this.groovyScriptEngine.eval(argString);
@@ -52,7 +55,7 @@ public final class GroovyCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return null;
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 61b27e7..149044a 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -5,6 +5,7 @@ import java.util.TreeMap;
 import java.util.stream.Collectors;
 
 import com.google.inject.Inject;
+import com.google.inject.Injector;
 
 import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
@@ -15,9 +16,13 @@ import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 import org.jetbrains.annotations.NotNull;
 
 public final class HelpCommand implements Command {
+	private final @NotNull Injector injector;
+	
 	@Inject
-	private HelpCommand() {
+	private HelpCommand(final @NotNull Injector injector) {
 		super();
+		
+		this.injector = injector;
 	}
 	
 	@Override
@@ -31,7 +36,8 @@ public final class HelpCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
 		final List<String> args = CommandUtils.splitArgs(argString);
 		if (args.isEmpty()) {
 			final StringBuilder sb = new StringBuilder("Type a valid B expression, or one of the following commands:\n");
@@ -75,10 +81,16 @@ public final class HelpCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final String prefix = argString.substring(0, at);
 		return new ReplacementOptions(
-			kernel.getCommands().keySet().stream().filter(s -> s.startsWith(prefix)).sorted().collect(Collectors.toList()),
+			this.injector.getInstance(ProBKernel.class)
+				.getCommands()
+				.keySet()
+				.stream()
+				.filter(s -> s.startsWith(prefix))
+				.sorted()
+				.collect(Collectors.toList()),
 			0,
 			argString.length()
 		);
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index c5e1559..5b69cb1 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -10,7 +10,6 @@ import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -39,7 +38,7 @@ public final class InitialiseCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString);
 		final Transition op = trace.getCurrentState().findTransition("$initialise_machine", predicates);
@@ -58,7 +57,7 @@ public final class InitialiseCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index 19b5c52..9ed0fe3 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -9,7 +9,6 @@ import de.prob.scripting.ClassicalBFactory;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -41,7 +40,7 @@ public final class LoadCellCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final String[] split = argString.split("\n", 2);
 		if (split.length != 2) {
 			throw new UserErrorException("Missing command body");
@@ -56,7 +55,7 @@ public final class LoadCellCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final int newlinePos = argString.indexOf('\n');
 		if (newlinePos == -1 || at < newlinePos) {
 			// Cursor is on the first line, provide preference name completions.
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index e1c93ab..5552b87 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -17,7 +17,6 @@ import de.prob.scripting.ModelTranslationError;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -54,7 +53,7 @@ public final class LoadFileCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final List<String> args = CommandUtils.splitArgs(argString);
 		if (args.isEmpty()) {
 			throw new UserErrorException("Missing machine file name");
@@ -72,7 +71,7 @@ public final class LoadFileCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final int fileNameEnd;
 		final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
 		if (argSplitMatcher.find()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
index 43d9bcb..7c77569 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
@@ -12,7 +12,6 @@ import de.prob.animator.command.GetPreferenceCommand;
 import de.prob.animator.command.SetPreferenceCommand;
 import de.prob.statespace.AnimationSelector;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -42,7 +41,7 @@ public final class PrefCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final List<String> args = CommandUtils.splitArgs(argString);
 		final StringBuilder sb = new StringBuilder();
 		if (args.isEmpty()) {
@@ -86,7 +85,7 @@ public final class PrefCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInPreferences(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
index 6d5a644..4d53205 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
@@ -7,8 +7,6 @@ import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.animator.domainobjects.IEvalElement;
 import de.prob.statespace.AnimationSelector;
 
-import de.prob2.jupyter.ProBKernel;
-
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -35,7 +33,7 @@ public final class PrettyPrintCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final IEvalElement formula = this.animationSelector.getCurrentTrace().getModel().parseFormula(argString, FormulaExpand.EXPAND);
 		
 		final PrettyPrintFormulaCommand cmdUnicode = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.UNICODE);
@@ -50,7 +48,7 @@ public final class PrettyPrintCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
index 0965634..149bb83 100644
--- a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
@@ -2,7 +2,6 @@ package de.prob2.jupyter.commands;
 
 import com.google.inject.Inject;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -28,7 +27,7 @@ public final class RenderCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final String[] split = argString.split("\n", 2);
 		if (split.length != 2) {
 			throw new UserErrorException("Missing content (the content cannot be placed on the same line as the command)");
@@ -44,7 +43,7 @@ public final class RenderCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return null;
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
index fd8dc29..f9df36f 100644
--- a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
@@ -9,7 +9,6 @@ import de.prob.animator.command.GetImagesForStateCommand;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -39,7 +38,7 @@ public final class ShowCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		if (!argString.isEmpty()) {
 			throw new UserErrorException("Expected no arguments");
 		}
@@ -73,7 +72,7 @@ public final class ShowCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return null;
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index f4b2d96..02ab8f5 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -13,7 +13,6 @@ import de.prob.animator.domainobjects.IEvalElement;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -42,7 +41,7 @@ public final class SolveCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final List<String> split = CommandUtils.splitArgs(argString, 2);
 		if (split.size() != 2) {
 			throw new UserErrorException("Expected 2 arguments, got 1");
@@ -82,7 +81,7 @@ public final class SolveCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final int solverNameEnd;
 		final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
 		if (argSplitMatcher.find()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index 0d22227..d79fc15 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
@@ -14,8 +14,6 @@ import de.prob.animator.domainobjects.TableData;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
-
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -42,7 +40,7 @@ public final class TableCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final IEvalElement formula = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
 		
@@ -83,7 +81,7 @@ public final class TableCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
index 9148485..5a89edd 100644
--- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
@@ -1,6 +1,7 @@
 package de.prob2.jupyter.commands;
 
 import com.google.inject.Inject;
+import com.google.inject.Injector;
 
 import de.prob2.jupyter.ProBKernel;
 
@@ -13,9 +14,13 @@ import org.jetbrains.annotations.Nullable;
 public final class TimeCommand implements Command {
 	private static final long NANOSECONDS_PER_SECOND = 1000000000L;
 	
+	private final @NotNull Injector injector;
+	
 	@Inject
-	private TimeCommand() {
+	private TimeCommand(final @NotNull Injector injector) {
 		super();
+		
+		this.injector = injector;
 	}
 	
 	@Override
@@ -29,7 +34,8 @@ public final class TimeCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @Nullable DisplayData run(final @NotNull String argString) {
+		final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
 		final long startTime = System.nanoTime();
 		final DisplayData result = kernel.eval(argString);
 		final long stopTime = System.nanoTime();
@@ -42,7 +48,7 @@ public final class TimeCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
-		return kernel.complete(argString, at);
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+		return this.injector.getInstance(ProBKernel.class).complete(argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 13167c4..df66411 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -9,8 +9,6 @@ import de.prob.exception.ProBError;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
-import de.prob2.jupyter.ProBKernel;
-
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -37,7 +35,7 @@ public final class TypeCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final IEvalElement formula = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
 		final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
@@ -49,7 +47,7 @@ public final class TypeCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
 	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
index ad3d097..83b11d7 100644
--- a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
@@ -6,8 +6,6 @@ import de.prob.Main;
 import de.prob.animator.command.GetVersionCommand;
 import de.prob.statespace.AnimationSelector;
 
-import de.prob2.jupyter.ProBKernel;
-
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 
@@ -35,14 +33,14 @@ public final class VersionCommand implements Command {
 	}
 	
 	@Override
-	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull String argString) {
 		final GetVersionCommand cmd = new GetVersionCommand();
 		this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
 		return new DisplayData(String.format("ProB CLI: %s\nProB 2: %s (%s)", cmd.getVersion(), Main.getVersion(), Main.getGitSha()));
 	}
 	
 	@Override
-	public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return null;
 	}
 }
-- 
GitLab