From be1480e223a7687b5bb20c4e3a3ef36cfb28c71e Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 17 Feb 2020 15:15:02 +0100
Subject: [PATCH] Expand :help intro text
---
notebooks/tests/help.ipynb | 115 ++++++++++--------
.../prob2/jupyter/commands/HelpCommand.java | 4 +-
2 files changed, 65 insertions(+), 54 deletions(-)
diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
index d941068..58842a6 100644
--- a/notebooks/tests/help.ipynb
+++ b/notebooks/tests/help.ipynb
@@ -15,61 +15,72 @@
{
"data": {
"text/markdown": [
- "Type a valid B expression, or one of the following commands:\n",
+ "Enter a B expression or predicate to evaluate it.\n",
"\n",
- "* `::load` Load the machine source code given in the cell body.\n",
- "* `::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.\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",
- "* `:load` Load the machine from the given path.\n",
- "* `:pref` View or change the value of one or more preferences.\n",
- "* `: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"
+ "You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
+ "\n",
+ "* `::load` - Load the machine source code given in the cell body.\n",
+ "* `::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",
+ "* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\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.\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",
+ "* `:let` - Evaluate an expression and store it in a local variable.\n",
+ "* `:load` - Load the machine from the given path.\n",
+ "* `:modelcheck` - Run the ProB model checker on the current model.\n",
+ "* `:pref` - View or change the value of one or more preferences.\n",
+ "* `: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",
+ "* `:unlet` - Remove a local variable.\n",
+ "* `:version` - Display version info about the ProB CLI and ProB 2.\n"
],
"text/plain": [
- "Type a valid B expression, or one of the following commands:\n",
- "::load Load the machine source code given in the cell body.\n",
- "::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.\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",
- ":load Load the machine from the given path.\n",
- ":pref View or change the value of one or more preferences.\n",
- ":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"
+ "Enter a B expression or predicate to evaluate it.\n",
+ "You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
+ "::load - Load the machine source code given in the cell body.\n",
+ "::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",
+ ":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\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.\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",
+ ":let - Evaluate an expression and store it in a local variable.\n",
+ ":load - Load the machine from the given path.\n",
+ ":modelcheck - Run the ProB model checker on the current model.\n",
+ ":pref - View or change the value of one or more preferences.\n",
+ ":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",
+ ":unlet - Remove a local variable.\n",
+ ":version - Display version info about the ProB CLI and ProB 2.\n"
]
},
"execution_count": 1,
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 9355b91..31badb3 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -46,8 +46,8 @@ public final class HelpCommand implements Command {
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");
- final StringBuilder sbMarkdown = new StringBuilder("Type a valid B expression, or one of the following commands:\n\n");
+ final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it.\nYou can also use any of the following commands. For more help on a particular command, run :help commandname.\n");
+ final StringBuilder sbMarkdown = new StringBuilder("Enter a B expression or predicate to evaluate it.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n\n");
new TreeMap<>(kernel.getCommands()).forEach((commandName, command) -> {
sb.append(commandName);
sb.append(" - ");
--
GitLab