From dc92a2a80bdc8a5d865157ee128ee9af64988869 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 19 Jul 2018 18:31:06 +0200
Subject: [PATCH] Support inspection in all commands that accept B formulas

---
 .../prob2/jupyter/commands/AssertCommand.java |  6 ++++
 .../prob2/jupyter/commands/CommandUtils.java  | 28 ++++++++++++++++++-
 .../jupyter/commands/ConstantsCommand.java    |  6 ++++
 .../de/prob2/jupyter/commands/DotCommand.java |  9 ++++++
 .../prob2/jupyter/commands/ExecCommand.java   |  9 ++++++
 .../prob2/jupyter/commands/FindCommand.java   |  6 ++++
 .../jupyter/commands/InitialiseCommand.java   |  6 ++++
 .../jupyter/commands/LoadCellCommand.java     | 12 ++++++++
 .../jupyter/commands/PrettyPrintCommand.java  |  6 ++++
 .../prob2/jupyter/commands/SolveCommand.java  |  9 ++++++
 .../prob2/jupyter/commands/TableCommand.java  |  6 ++++
 .../prob2/jupyter/commands/TimeCommand.java   |  5 ++++
 .../prob2/jupyter/commands/TypeCommand.java   |  6 ++++
 13 files changed, 113 insertions(+), 1 deletion(-)

diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index b77cb0c..68a7588 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
index 0dbdbf1..fce3cd2 100644
--- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
+++ b/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.
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 8dbbacc..9532f64 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index 6b2aeca..989ccf9 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/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(
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index ed7f52f..9ebd093 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/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(
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index 03cbfd3..09e0bb8 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 33c1f55..3ec63d9 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index 9213744..0727356 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/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');
diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
index 33c2a2d..118eed3 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index da3e585..b12b289 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/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(
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index 494fe05..1043cf3 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
index 7ce1902..2bff95b 100644
--- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index fcb3d26..6474646 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/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);
-- 
GitLab