diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb index 58842a6b85bb1d17057ba8e853b59db2e7ba5852..cbcb887c0136e3838cdc367f2ce9fd33f617c14b 100644 --- a/notebooks/tests/help.ipynb +++ b/notebooks/tests/help.ipynb @@ -19,67 +19,91 @@ "\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", + "## Evaluation\n", + "\n", + "* `:eval` - Evaluate a formula and display the result.\n", + "* `:solve` - Solve a predicate with the specified solver.\n", + "* `:table` - Display an expression as a table.\n", + "* `:type` - Display the type of a formula.\n", + "* `:prettyprint` - Pretty-print a predicate.\n", + "* `:let` - Evaluate an expression and store it in a local variable.\n", + "* `:unlet` - Remove a local variable.\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", + "\n", + "## Animation\n", + "\n", + "* `::load` - Load the machine source code given in the cell body.\n", + "* `:load` - Load the machine from the given path.\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", + "* `:init` - Initialise the current machine with the specified predicate\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", + "* `:browse` - Show information about the current state.\n", + "* `:trace` - Display all states and transitions in the current trace.\n", "* `:goto` - Go to the state with the specified index in the current trace.\n", + "* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n", + "\n", + "## Visualisation\n", + "\n", + "* `:show` - Show the machine's animation function visualisation for the current state.\n", + "* `:dot` - Execute and show a dot visualisation.\n", + "\n", + "## Verification\n", + "\n", + "* `:check` - Check the machine's properties, invariant, or assertions in the current state.\n", + "* `:modelcheck` - Run the ProB model checker on the current model.\n", + "\n", + "## Other\n", + "\n", + "* `::render` - Render some content with the specified MIME type.\n", + "* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\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": [ "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", + "\n", + "Evaluation:\n", + ":eval - Evaluate a formula and display the result.\n", + ":solve - Solve a predicate with the specified solver.\n", + ":table - Display an expression as a table.\n", + ":type - Display the type of a formula.\n", + ":prettyprint - Pretty-print a predicate.\n", + ":let - Evaluate an expression and store it in a local variable.\n", + ":unlet - Remove a local variable.\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", + "\n", + "Animation:\n", + "::load - Load the machine source code given in the cell body.\n", + ":load - Load the machine from the given path.\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", + ":init - Initialise the current machine with the specified predicate\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", + ":browse - Show information about the current state.\n", + ":trace - Display all states and transitions in the current trace.\n", ":goto - Go to the state with the specified index in the current trace.\n", + ":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n", + "\n", + "Visualisation:\n", + ":show - Show the machine's animation function visualisation for the current state.\n", + ":dot - Execute and show a dot visualisation.\n", + "\n", + "Verification:\n", + ":check - Check the machine's properties, invariant, or assertions in the current state.\n", + ":modelcheck - Run the ProB model checker on the current model.\n", + "\n", + "Other:\n", + "::render - Render some content with the specified MIME type.\n", + ":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\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" ] }, diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java index 51213685c787d9a98c58995a571c6397a376fa70..c8a510a3266a98af6c97c5477e56f04869830217 100644 --- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java @@ -1,7 +1,12 @@ package de.prob2.jupyter.commands; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.Comparator; +import java.util.LinkedHashMap; import java.util.List; -import java.util.TreeMap; +import java.util.Map; import java.util.stream.Collectors; import com.google.inject.Inject; @@ -17,6 +22,41 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; public final class HelpCommand implements Command { + private static final @NotNull Map<@NotNull String, @NotNull List<@NotNull Class<? extends Command>>> COMMAND_CLASS_CATEGORIES; + static { + final Map<String, List<Class<? extends Command>>> commandCategories = new LinkedHashMap<>(); + commandCategories.put("Evaluation", Collections.unmodifiableList(Arrays.asList( + EvalCommand.class, + SolveCommand.class, + TableCommand.class, + TypeCommand.class, + PrettyPrintCommand.class, + LetCommand.class, + UnletCommand.class, + AssertCommand.class + ))); + commandCategories.put("Animation", Collections.unmodifiableList(Arrays.asList( + LoadCellCommand.class, + LoadFileCommand.class, + ConstantsCommand.class, + InitialiseCommand.class, + ExecCommand.class, + BrowseCommand.class, + TraceCommand.class, + GotoCommand.class, + FindCommand.class + ))); + commandCategories.put("Visualisation", Collections.unmodifiableList(Arrays.asList( + ShowCommand.class, + DotCommand.class + ))); + commandCategories.put("Verification", Collections.unmodifiableList(Arrays.asList( + CheckCommand.class, + ModelCheckCommand.class + ))); + COMMAND_CLASS_CATEGORIES = Collections.unmodifiableMap(commandCategories); + } + private final @NotNull Injector injector; @Inject @@ -52,18 +92,50 @@ public final class HelpCommand implements Command { final List<String> args = CommandUtils.splitArgs(argString); if (args.isEmpty()) { 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(" - "); - sb.append(command.getShortHelp()); - sb.append('\n'); - sbMarkdown.append("* `"); - sbMarkdown.append(commandName); - sbMarkdown.append("` - "); - sbMarkdown.append(command.getShortHelp()); - sbMarkdown.append('\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"); + + final Map<Class<? extends Command>, Command> commandsByClass = kernel.getCommands() + .values() + .stream() + .collect(Collectors.toMap( + command -> command.getClass().asSubclass(Command.class), + command -> command + )); + final Map<String, List<Command>> commandCategories = new LinkedHashMap<>(); + COMMAND_CLASS_CATEGORIES.forEach((categoryName, commandClasses) -> + commandCategories.put( + categoryName, + commandClasses.stream() + .map(commandsByClass::get) + .collect(Collectors.toList()) + ) + ); + final List<Command> uncategorizedCommands = new ArrayList<>(kernel.getCommands().values()); + commandCategories.values().forEach(uncategorizedCommands::removeAll); + uncategorizedCommands.sort(Comparator.comparing(Command::getName)); + commandCategories.put("Other", uncategorizedCommands); + + commandCategories.forEach((categoryName, commands) -> { + sb.append("\n"); + sb.append(categoryName); + sb.append(":\n"); + sbMarkdown.append("\n## "); + sbMarkdown.append(categoryName); + sbMarkdown.append("\n\n"); + + commands.forEach(command -> { + sb.append(command.getName()); + sb.append(" - "); + sb.append(command.getShortHelp()); + sb.append('\n'); + sbMarkdown.append("* `"); + sbMarkdown.append(command.getName()); + sbMarkdown.append("` - "); + sbMarkdown.append(command.getShortHelp()); + sbMarkdown.append('\n'); + }); }); + final DisplayData result = new DisplayData(sb.toString()); result.putMarkdown(sbMarkdown.toString()); return result;