diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index e51914ffb2e645670c7395cdfba02a47f1fea873..9fdb4e74c0921acd4a1ce0fef11b411b4e2d4f29 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 7c311174aab0b8c92f51ff5473f2f561dea3ba8b..ab8cfc086698cc05a21726cea0dea14d99dfcae2 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 050c1dfb5d94d8d020a87ac5d854a73ca8ea1ee2..df7eeec4d25afd17e4ce444d433633f294bdf152 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 5f30dd61756af2fc00f828f3895f487daf130bc1..7c7f5a35da20394f55fd2a85a208fab6fd24c55a 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 2535c0dd616df4c885edbf8952c9f775c32fbca0..ca2550221f97916c3924a0db4323a8065b27f20d 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 6d8d55653e051915e861613ae982046f63080acb..54fc9e5b26f8691cad6dde8cf8b9a8d5d33d872f 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 4b915f5dc7e82634e67bed9adb35d9116774e1a0..87d426b8578cc411f0e69b0733f1e0d2d239d7f8 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 31774a1e89d4e48f5331e0c2052c4322d8e65f13..c74e114594b3a4158a5558d46f333fc27de355e4 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 3d28c1acb87c422a645caf52a3b87b89b2970eb1..b66513276adcba55ead84460488cc4a1a2067e45 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 61b27e75e121d0e52e28c1aa3cb1234a29ee35c6..149044a83652c0ab3bdd127f4e4c839f099784f1 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 c5e155978851cbdcec256023a2a267c0e33a194e..5b69cb1de03cc7bfbbe989f66f44132bb658261f 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 19b5c525fd1508110587710a20d90927870cf319..9ed0fe3a485aa047e8cdda5d2906c1c896ebe31b 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 e1c93abfb7d5f63db92f2ca4334db5926f7b72c2..5552b8799373b3ef488e3c6958a3bccfa77ea460 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 43d9bcb2be9815bcbbf9027958ad002aa9da58da..7c77569b0b974dffc808e0b500849b08c5ab3e1a 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 6d5a6442c454c4d0c40c205a119c63a8f6938adc..4d532050266098b17bcb68c2032e822fcd12d267 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 0965634d80b6c8a42d012e39cb84d6cd15285d5b..149bb8373153ed6501c1853cc73278929ca422fb 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 fd8dc29e8822f299e2c4ed912fa6311ff7cc7da3..f9df36fb0e04fc70f270330be14829c6b3539b98 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 f4b2d960bc48db89e45f3e661206714c39c9638c..02ab8f52977c3b333ea4b855c9340e64083dbf8e 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 0d22227c1528240158861493f1bf0aa330da7b18..d79fc154308ed14f79c165c6d21fa0086c5a5980 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 9148485ad81e64874adbd52ec594e46bb17f146b..5a89edd1208d46786c32f9849bea5e2beba8a254 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 13167c49805e0b5392f0d47c4789abd7810c584e..df66411a63d29f3b0ca2563d897288e684ba2880 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 ad3d097b6d46ded82c09343b9d7a72ce5fafa4b3..83b11d749e339bc05827aba5ddbf872c68c72596 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;
 	}
 }