Add initial support for inspection (Shift-Tab in Jupyter Notebook)

notebooks/tests/help.ipynb

@@ -21,10 +21,13 @@
        "* `::render` Render some content with the specified MIME type.\n",
        "* `:assert` Ensure that the predicate is true, and show an error otherwise.\n",
        "* `:browse` Show information about the current state.\n",
+       "* `:check` Check the machine's properties, invariant, or assertions in the current state.\n",
        "* `:constants` Set up the current machine's constants.\n",
        "* `:dot` Execute and show a dot visualisation.\n",
        "* `:eval` Evaluate a formula and display the result.\n",
-       "* `:exec` Execute an operation with the specified predicate, or by its ID.\n",
+       "* `:exec` Execute an operation.\n",
+       "* `:find` Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
+       "* `:goto` Go to the state with the specified index in the current trace.\n",
        "* `:groovy` Evaluate the given Groovy expression.\n",
        "* `:help` Display help for a specific command, or general help about the REPL.\n",
        "* `:init` Initialise the current machine with the specified predicate\n",
@@ -33,8 +36,10 @@
        "* `:prettyprint` Pretty-print a predicate.\n",
        "* `:show` Show the machine's animation function visualisation for the current state.\n",
        "* `:solve` Solve a predicate with the specified solver.\n",
+       "* `:stats` Show statistics about the state space.\n",
        "* `:table` Display an expression as a table.\n",
        "* `:time` Execute the given command and measure how long it takes to execute.\n",
+       "* `:trace` Display all states and transitions in the current trace.\n",
        "* `:type` Display the type of a formula.\n",
        "* `:version` Display version info about the ProB CLI and ProB 2.\n"
       ],
@@ -44,10 +49,13 @@
        "::render Render some content with the specified MIME type.\n",
        ":assert Ensure that the predicate is true, and show an error otherwise.\n",
        ":browse Show information about the current state.\n",
+       ":check Check the machine's properties, invariant, or assertions in the current state.\n",
        ":constants Set up the current machine's constants.\n",
        ":dot Execute and show a dot visualisation.\n",
        ":eval Evaluate a formula and display the result.\n",
-       ":exec Execute an operation with the specified predicate, or by its ID.\n",
+       ":exec Execute an operation.\n",
+       ":find Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
+       ":goto Go to the state with the specified index in the current trace.\n",
        ":groovy Evaluate the given Groovy expression.\n",
        ":help Display help for a specific command, or general help about the REPL.\n",
        ":init Initialise the current machine with the specified predicate\n",
@@ -56,8 +64,10 @@
        ":prettyprint Pretty-print a predicate.\n",
        ":show Show the machine's animation function visualisation for the current state.\n",
        ":solve Solve a predicate with the specified solver.\n",
+       ":stats Show statistics about the state space.\n",
        ":table Display an expression as a table.\n",
        ":time Execute the given command and measure how long it takes to execute.\n",
+       ":trace Display all states and transitions in the current trace.\n",
        ":type Display the type of a formula.\n",
        ":version Display version info about the ProB CLI and ProB 2.\n"
       ]

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -254,6 +254,38 @@ public final class ProBKernel extends BaseKernel {
 		return this.executeCommand(":eval", expr);
 	}
 	
+	@Override
+	public @Nullable DisplayData inspect(final @NotNull String code, final int at, final boolean extraDetail) {
+		// Note: We ignore the extraDetail parameter, because in practice it is always false. This is because the inspect_request messages sent by Jupyter Notebook always have their detail_level set to 0.
+		final Matcher commandMatcher = COMMAND_PATTERN.matcher(code);
+		if (commandMatcher.matches()) {
+			// The code is a valid command.
+			final int argOffset = commandMatcher.start(2);
+			final String name = commandMatcher.group(1);
+			if (this.getCommands().containsKey(name)) {
+				final Command command = this.getCommands().get(name);
+				if (at <= commandMatcher.end(1)) {
+					// The cursor is somewhere in the command name, show help text for the command.
+					return command.renderHelp();
+				} else if (at < commandMatcher.start(2)) {
+					// The cursor is in the whitespace between the command name and arguments, don't show anything.
+					return null;
+				} else {
+					// The cursor is somewhere in the command arguments, ask the command to inspect.
+					assert name != null;
+					final String argString = commandMatcher.group(2) == null ? "" : commandMatcher.group(2);
+					return command.inspect(argString, at - argOffset);
+				}
+			} else {
+				// Invalid command, can't inspect.
+				return null;
+			}
+		} else {
+			// The code is not a valid command, ask :eval to inspect.
+			return this.getCommands().get(":eval").inspect(code, at);
+		}
+	}
+	
 	@Override
 	public @Nullable ReplacementOptions complete(final @NotNull String code, final int at) {
 		final Matcher commandMatcher = COMMAND_PATTERN.matcher(code);

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

@@ -13,7 +13,35 @@ public interface Command {
 	
 	public abstract @NotNull String getHelpBody();
 	
+	public default @NotNull DisplayData renderHelp() {
+		final StringBuilder sbPlain = new StringBuilder();
+		final StringBuilder sbMarkdown = new StringBuilder();
+		sbPlain.append(this.getSyntax());
+		sbPlain.append('\n');
+		sbMarkdown.append("```\n");
+		sbMarkdown.append(this.getSyntax());
+		sbMarkdown.append("\n```\n\n");
+		
+		final String shortHelp = this.getShortHelp();
+		sbPlain.append(shortHelp);
+		sbMarkdown.append(shortHelp);
+		final String helpBody = this.getHelpBody();
+		if (!helpBody.isEmpty()) {
+			sbPlain.append("\n\n");
+			sbPlain.append(helpBody);
+			sbMarkdown.append("\n\n");
+			sbMarkdown.append(helpBody);
+		}
+		final DisplayData result = new DisplayData(sbPlain.toString());
+		result.putMarkdown(sbMarkdown.toString());
+		return result;
+	}
+	
 	public abstract @Nullable DisplayData run(final @NotNull String argString);
 	
+	public default @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
+		return null;
+	}
+	
 	public abstract @Nullable ReplacementOptions complete(final @NotNull String argString, final int at);
 }

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

@@ -77,19 +77,7 @@ public final class HelpCommand implements Command {
 			if (command == null) {
 				throw new UserErrorException(String.format("Cannot display help for unknown command \"%s\"", commandName));
 			}
-			final StringBuilder sb = new StringBuilder();
-			sb.append("```\n");
-			sb.append(command.getSyntax());
-			sb.append("\n```\n\n");
-			sb.append(command.getShortHelp());
-			final String helpBody = command.getHelpBody();
-			if (!helpBody.isEmpty()) {
-				sb.append("\n\n");
-				sb.append(helpBody);
-			}
-			final DisplayData result = new DisplayData(sb.toString());
-			result.putMarkdown(sb.toString());
-			return result;
+			return command.renderHelp();
 		} else {
 			throw new UserErrorException("Expected at most 1 argument, got " + args.size());
 		}