Add command system and a help command

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

 package de.prob2.jupyter;
 
+import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 import com.google.inject.Inject;
 
@@ -10,42 +16,75 @@ import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.scripting.ClassicalBFactory;
 import de.prob.statespace.Trace;
 
-import org.jetbrains.annotations.NotNull;
+import de.prob2.jupyter.commands.CommandExecutionException;
+import de.prob2.jupyter.commands.HelpCommand;
+import de.prob2.jupyter.commands.NoSuchCommandException;
+import de.prob2.jupyter.commands.ReplCommand;
 
 import io.github.spencerpark.jupyter.kernel.BaseKernel;
 import io.github.spencerpark.jupyter.kernel.LanguageInfo;
 import io.github.spencerpark.jupyter.messages.DisplayData;
 
+import org.jetbrains.annotations.NotNull;
+
 public class ProBKernel extends BaseKernel {
+	private static final Pattern COMMAND_PATTERN = Pattern.compile("\\s*\\:(.*)");
+	
+	private final @NotNull Map<@NotNull String, @NotNull ReplCommand> commands;
 	private @NotNull Trace trace;
 	
 	@Inject
 	private ProBKernel(final @NotNull ClassicalBFactory classicalBFactory) {
 		super();
 		
+		this.commands = new HashMap<>();
+		final ReplCommand help = new HelpCommand();
+		this.commands.put("?", help);
+		this.commands.put("help", help);
 		this.trace = new Trace(classicalBFactory.create("MACHINE repl END").load());
 	}
 	
+	public @NotNull Map<@NotNull String, @NotNull ReplCommand> getCommands() {
+		return Collections.unmodifiableMap(this.commands);
+	}
+	
 	@Override
-	public String getBanner() {
+	public @NotNull String getBanner() {
 		return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";
 	}
 	
 	@Override
-	public List<LanguageInfo.Help> getHelpLinks() {
+	public @NotNull List<LanguageInfo.@NotNull Help> getHelpLinks() {
 		return Collections.singletonList(new LanguageInfo.Help("ProB User Manual", "https://www3.hhu.de/stups/prob/index.php/User_Manual"));
 	}
 	
+	private @NotNull DisplayData executeCommand(final @NotNull String name, final @NotNull List<@NotNull String> args) {
+		final ReplCommand command = this.getCommands().get(name);
+		if (command == null) {
+			throw new NoSuchCommandException(name);
+		}
+		return command.run(this, name, args);
+	}
+	
 	@Override
-	public DisplayData eval(final String expr) {
+	public @NotNull DisplayData eval(final String expr) {
 		assert expr != null;
 		
+		final Matcher matcher = COMMAND_PATTERN.matcher(expr);
+		if (matcher.matches()) {
+			final List<String> args = new ArrayList<>(Arrays.asList(matcher.group(1).split("\\s+")));
+			// args always contains at least one element, even for an empty string (in that case the only element is an empty string).
+			assert args.size() >= 1;
+			final String name = args.remove(0);
+			return this.executeCommand(name, args);
+		} else {
 			final AbstractEvalResult result = this.trace.evalCurrent(expr, FormulaExpand.EXPAND);
 			return new DisplayData(result.toString());
 		}
+	}
 	
 	@Override
-	public LanguageInfo getLanguageInfo() {
+	public @NotNull LanguageInfo getLanguageInfo() {
 		return new LanguageInfo.Builder("prob")
 			.mimetype("text/x-prob")
 			.fileExtension(".prob")
@@ -56,4 +95,13 @@ public class ProBKernel extends BaseKernel {
 	public void onShutdown(final boolean isRestarting) {
 		this.trace.getStateSpace().kill();
 	}
+	
+	@Override
+	public @NotNull List<@NotNull String> formatError(final Exception e) {
+		if (e instanceof NoSuchCommandException || e instanceof CommandExecutionException) {
+			return this.errorStyler.secondaryLines(e.getMessage());
+		} else {
+			return super.formatError(e);
+		}
+	}
 }

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

+package de.prob2.jupyter.commands;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class CommandExecutionException extends RuntimeException {
+	private static final long serialVersionUID = 1L;
+	
+	private final @NotNull String commandName;
+	
+	public CommandExecutionException(final @NotNull String commandName, final @NotNull String message, final @Nullable Throwable cause) {
+		super(formatMessage(commandName, message), cause);
+		
+		this.commandName = commandName;
+	}
+	
+	public CommandExecutionException(final @NotNull String commandName, final @NotNull String message) {
+		this(commandName, message, null);
+	}
+	
+	private static @NotNull String formatMessage(final @NotNull String commandName, final @NotNull String message) {
+		return String.format(":%s: %s", commandName, message);
+	}
+	
+	public @NotNull String getCommandName() {
+		return this.commandName;
+	}
+}

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

+package de.prob2.jupyter.commands;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+
+import de.prob2.jupyter.ProBKernel;
+
+import io.github.spencerpark.jupyter.messages.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class HelpCommand implements ReplCommand {
+	@Override
+	public @NotNull String getSyntax() {
+		return ":? [COMMAND]\n:help [COMMAND]";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Display help for a specific command, or general help about the REPL.";
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull List<@NotNull String> args) {
+		if (args.isEmpty()) {
+			final StringBuilder sb = new StringBuilder("Type a valid B expression, or one of the following commands:\n");
+			final List<String> names = new ArrayList<>(kernel.getCommands().keySet());
+			Collections.sort(names);
+			for (final String commandName : names) {
+				final ReplCommand command = kernel.getCommands().get(commandName);
+				assert command != null;
+				sb.append(':');
+				sb.append(commandName);
+				sb.append(' ');
+				sb.append(command.getShortHelp());
+				sb.append('\n');
+			}
+			return new DisplayData(sb.toString());
+		} else if (args.size() == 1) {
+			final String commandName = args.get(0);
+			final ReplCommand command = kernel.getCommands().get(commandName);
+			if (command == null) {
+				throw new CommandExecutionException(name, String.format("Cannot display help for unknown command \"%s\"", commandName));
+			}
+			return new DisplayData(command.getLongHelp());
+		} else {
+			throw new CommandExecutionException(name, "Expected at most 1 argument, got " + args.size());
+		}
+	}
+}

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

+package de.prob2.jupyter.commands;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class NoSuchCommandException extends RuntimeException {
+	private static final long serialVersionUID = 1L;
+	
+	private final @NotNull String name;
+	
+	public NoSuchCommandException(final @NotNull String name, final @Nullable String message, final @Nullable Throwable cause) {
+		super(formatMessage(name, message), cause);
+		
+		this.name = name;
+	}
+	
+	public NoSuchCommandException(final @NotNull String name, final @Nullable String message) {
+		this(name, message, null);
+	}
+	
+	public NoSuchCommandException(final @NotNull String name, final @Nullable Throwable cause) {
+		this(name, null, cause);
+	}
+	
+	public NoSuchCommandException(final @NotNull String name) {
+		this(name, null, null);
+	}
+	
+	private static final @NotNull String formatMessage(final @NotNull String name, final @Nullable String message) {
+		final StringBuilder sb = new StringBuilder("Unknown command: \"");
+		sb.append(name);
+		sb.append('"');
+		if (message != null) {
+			sb.append(": ");
+			sb.append(message);
+		}
+		return sb.toString();
+	}
+	
+	public @NotNull String getName() {
+		return this.name;
+	}
+}

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

+package de.prob2.jupyter.commands;
+
+import java.util.List;
+
+import de.prob2.jupyter.ProBKernel;
+
+import io.github.spencerpark.jupyter.messages.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public interface ReplCommand {
+	public abstract @NotNull String getSyntax();
+	
+	public abstract @NotNull String getShortHelp();
+	
+	public default  @NotNull String getLongHelp() {
+		return this.getSyntax() + "\n\n" + this.getShortHelp();
+	}
+	
+	public abstract @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull List<@NotNull String> args);
+}