Support inspection in all commands that accept B formulas

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

@@ -14,6 +14,7 @@ import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 import io.github.spencerpark.jupyter.kernel.display.mime.MIMEType;
 
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 public final class AssertCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -58,6 +59,11 @@ public final class AssertCommand implements Command {
 		throw new UserErrorException("Assertion is not true: " + displayData.getData(MIMEType.TEXT_PLAIN));
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);

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

@@ -41,8 +41,14 @@ import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
 public final class CommandUtils {
+	@FunctionalInterface
+	public interface Inspector {
+		public abstract @Nullable DisplayData inspect(final @NotNull String argString, final int at);
+	}
+	
+	@FunctionalInterface
 	public interface Completer {
-		public abstract @Nullable ReplacementOptions complete(final @NotNull String argString, final int offset);
+		public abstract @Nullable ReplacementOptions complete(final @NotNull String argString, final int at);
 	}
 	
 	private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(CommandUtils.class);
@@ -227,6 +233,22 @@ public final class CommandUtils {
 		);
 	}
 	
+	public static @Nullable DisplayData inspectArgs(final @NotNull String argString, final int at, final @NotNull Inspector @NotNull... inspectors) {
+		final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(argString);
+		int argStart = 0;
+		int argEnd = argString.length();
+		int i = 0;
+		while (argSplitMatcher.find() && i < inspectors.length) {
+			if (argSplitMatcher.end() > at) {
+				argEnd = argSplitMatcher.start();
+				break;
+			}
+			argStart = argSplitMatcher.end();
+			i++;
+		}
+		return inspectors[i].inspect(argString.substring(argStart, argEnd), at - argStart);
+	}
+	
 	public static @Nullable ReplacementOptions completeArgs(final @NotNull String argString, final int at, final @NotNull Completer @NotNull... completers) {
 		final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(argString);
 		int argStart = 0;
@@ -298,6 +320,10 @@ public final class CommandUtils {
 		return result;
 	}
 	
+	public static @NotNull Inspector bExpressionInspector(final @NotNull Trace trace) {
+		return (code, at) -> inspectInBExpression(trace, code, at);
+	}
+	
 	public static @NotNull ReplacementOptions completeInBExpression(final @NotNull Trace trace, final @NotNull String code, final int at) {
 		final Matcher identifierMatcher = matchBIdentifierAt(code, at);
 		// Try to find the identifier that the cursor is in.

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

@@ -14,6 +14,7 @@ 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 ConstantsCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -52,6 +53,11 @@ public final class ConstantsCommand implements Command {
 		return new DisplayData(String.format("Machine constants set up using operation %s: %s", op.getId(), op.getRep()));
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);

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

@@ -117,6 +117,15 @@ public final class DotCommand implements Command {
 		return result;
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectArgs(
+			argString, at,
+			(commandName, at0) -> null, // TODO
+			CommandUtils.bExpressionInspector(this.animationSelector.getCurrentTrace())
+		);
+	}
+	
 	@Override
 	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeArgs(

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

@@ -59,6 +59,15 @@ public final class ExecCommand implements Command {
 		return new DisplayData(String.format("Executed operation: %s", op.getRep()));
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectArgs(
+			argString, at,
+			(operation, at0) -> null, // TODO
+			CommandUtils.bExpressionInspector(this.animationSelector.getCurrentTrace())
+		);
+	}
+	
 	@Override
 	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeArgs(

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

@@ -11,6 +11,7 @@ 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 FindCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -48,6 +49,11 @@ public final class FindCommand implements Command {
 		return new DisplayData("Found a matching state and made it current state");
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);

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

@@ -14,6 +14,7 @@ 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 InitialiseCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -52,6 +53,11 @@ public final class InitialiseCommand implements Command {
 		return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep()));
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);

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

@@ -62,6 +62,18 @@ public final class LoadCellCommand implements Command {
 		return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(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 inspections.
+			return null; // TODO
+		} else {
+			// Cursor is in the body, provide B inspections.
+			return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+		}
+	}
+	
 	@Override
 	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		final int newlinePos = argString.indexOf('\n');

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

@@ -11,6 +11,7 @@ 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 PrettyPrintCommand implements Command {
 	private final AnimationSelector animationSelector;
@@ -53,6 +54,11 @@ public final class PrettyPrintCommand implements Command {
 		return ret;
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);

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

@@ -75,6 +75,15 @@ public final class SolveCommand implements Command {
 		return CommandUtils.displayDataForEvalResult(cmd.getValue());
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectArgs(
+			argString, at,
+			(solverName, at0) -> null, // TODO
+			CommandUtils.bExpressionInspector(this.animationSelector.getCurrentTrace())
+		);
+	}
+	
 	@Override
 	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeArgs(

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

@@ -20,6 +20,7 @@ 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 TableCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -87,6 +88,11 @@ public final class TableCommand implements Command {
 		return res;
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);

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

@@ -53,6 +53,11 @@ public final class TimeCommand implements Command {
 		return result;
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return this.injector.getInstance(ProBKernel.class).inspect(argString, at, false);
+	}
+	
 	@Override
 	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return this.injector.getInstance(ProBKernel.class).complete(argString, at);

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

@@ -13,6 +13,7 @@ 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 TypeCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -51,6 +52,11 @@ public final class TypeCommand implements Command {
 		}
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+	
 	@Override
 	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
 		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);