From 137889ebb1c9384c99534cf98fc6a057acc95099 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 19 Jul 2018 16:55:54 +0200
Subject: [PATCH] Add initial support for inspection (Shift-Tab in Jupyter
Notebook)
---
notebooks/tests/help.ipynb | 14 ++++++--
.../java/de/prob2/jupyter/ProBKernel.java | 32 +++++++++++++++++++
.../de/prob2/jupyter/commands/Command.java | 30 ++++++++++++++++-
.../prob2/jupyter/commands/HelpCommand.java | 14 +-------
4 files changed, 74 insertions(+), 16 deletions(-)
diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
index 8489fd0..c37e3a7 100644
--- a/notebooks/tests/help.ipynb
+++ b/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"
]
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 46846d6..df2b0cf 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/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);
diff --git a/src/main/java/de/prob2/jupyter/commands/Command.java b/src/main/java/de/prob2/jupyter/commands/Command.java
index b9be2eb..fb906dc 100644
--- a/src/main/java/de/prob2/jupyter/commands/Command.java
+++ b/src/main/java/de/prob2/jupyter/commands/Command.java
@@ -11,9 +11,37 @@ public interface Command {
public abstract @NotNull String getShortHelp();
- public abstract @NotNull String getHelpBody();
+ 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);
}
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 42fb943..bfee912 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/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());
}
--
GitLab