diff --git a/src/main/java/de/prob2/jupyter/Command.java b/src/main/java/de/prob2/jupyter/Command.java
index ebeca7c7a170a289a70b6b56aa747f3fbf51f137..ee1361accd0fa0a7a9984fe7c81acafbd06dad36 100644
--- a/src/main/java/de/prob2/jupyter/Command.java
+++ b/src/main/java/de/prob2/jupyter/Command.java
@@ -9,6 +9,8 @@ import org.jetbrains.annotations.Nullable;
public interface Command {
public abstract @NotNull String getName();
+ public abstract @NotNull Parameters getParameters();
+
public abstract @NotNull String getSyntax();
public abstract @NotNull String getShortHelp();
@@ -39,7 +41,7 @@ public interface Command {
return result;
}
- public abstract @Nullable DisplayData run(final @NotNull String argString);
+ public abstract @Nullable DisplayData run(final @NotNull ParsedArguments args);
public abstract @Nullable DisplayData inspect(final @NotNull String argString, final int at);
diff --git a/src/main/java/de/prob2/jupyter/CommandUtils.java b/src/main/java/de/prob2/jupyter/CommandUtils.java
index e2b855a9907397ab9000ac1e64f9161a5e9bd991..3c83d96eb6a868411d65c2ff03b0d2141f36c78c 100644
--- a/src/main/java/de/prob2/jupyter/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/CommandUtils.java
@@ -2,6 +2,7 @@ package de.prob2.jupyter;
import java.util.ArrayList;
import java.util.Arrays;
+import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
@@ -101,6 +102,41 @@ public final class CommandUtils {
return splitArgs(args, 0);
}
+ private static <T> @NotNull String parseSingleArg(final @NotNull ParsedArguments parsed, final @NotNull String remainingArgs, final @NotNull PositionalParameter<T> param) {
+ final Parameter.ParseResult<T> parsedSingleArg = param.parse(remainingArgs);
+ parsed.put(param, parsedSingleArg.getParsedArg());
+ return parsedSingleArg.getRemainingArgString();
+ }
+
+ private static <T> void checkParsedParameter(final @NotNull ParsedArguments parsed, final @NotNull PositionalParameter<T> param) {
+ if (!parsed.containsKey(param)) {
+ if (param.isOptional()) {
+ parsed.put(param, param.getDefaultValue());
+ } else {
+ throw new UserErrorException("Missing required parameter " + param.getIdentifier());
+ }
+ }
+ }
+
+ public static @NotNull ParsedArguments parseArgs(final @NotNull Parameters parameters, final @NotNull String argString) {
+ final ParsedArguments parsed = new ParsedArguments(Collections.emptyMap());
+ String remainingArgs = argString;
+ for (final PositionalParameter<?> param : parameters.getPositionalParameters()) {
+ if (remainingArgs.isEmpty()) {
+ break;
+ }
+
+ remainingArgs = parseSingleArg(parsed, remainingArgs, param);
+ }
+ if (!remainingArgs.isEmpty()) {
+ throw new UserErrorException("Expected at most " + parameters.getPositionalParameters().size() + " arguments, got extra argument: " + remainingArgs);
+ }
+ for (final PositionalParameter<?> param : parameters.getPositionalParameters()) {
+ checkParsedParameter(parsed, param);
+ }
+ return parsed;
+ }
+
public static @NotNull Map<@NotNull String, @NotNull String> parsePreferences(final @NotNull List<@NotNull String> args) {
final Map<String, String> preferences = new HashMap<>();
for (final String arg : args) {
diff --git a/src/main/java/de/prob2/jupyter/Parameter.java b/src/main/java/de/prob2/jupyter/Parameter.java
new file mode 100644
index 0000000000000000000000000000000000000000..bb1fcb93a474bfe18f1b44919d2eb60692d3a84e
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/Parameter.java
@@ -0,0 +1,52 @@
+package de.prob2.jupyter;
+
+import com.google.common.base.MoreObjects;
+
+import org.jetbrains.annotations.NotNull;
+
+public abstract class Parameter<T> {
+ public static final class ParseResult<T> {
+ private final T parsedArg;
+ private final @NotNull String remainingArgString;
+
+ public ParseResult(final T parsedArg, final @NotNull String remainingArgString) {
+ super();
+
+ this.parsedArg = parsedArg;
+ this.remainingArgString = remainingArgString;
+ }
+
+ public T getParsedArg() {
+ return this.parsedArg;
+ }
+
+ public @NotNull String getRemainingArgString() {
+ return this.remainingArgString;
+ }
+ }
+
+ private final @NotNull String identifier;
+
+ protected Parameter(final @NotNull String identifier) {
+ super();
+
+ this.identifier = identifier;
+ }
+
+ public @NotNull String getIdentifier() {
+ return this.identifier;
+ }
+
+ public abstract boolean isOptional();
+
+ public abstract T getDefaultValue();
+
+ public abstract Parameter.ParseResult<T> parse(final @NotNull String argString);
+
+ @Override
+ public String toString() {
+ return MoreObjects.toStringHelper(this)
+ .add("identifier", this.getIdentifier())
+ .toString();
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/Parameters.java b/src/main/java/de/prob2/jupyter/Parameters.java
new file mode 100644
index 0000000000000000000000000000000000000000..0ef54274217db75f79a4a4970ddf06e02b439223
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/Parameters.java
@@ -0,0 +1,37 @@
+package de.prob2.jupyter;
+
+import java.util.Collections;
+import java.util.List;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class Parameters {
+ public static final @NotNull Parameters NONE = new Parameters(Collections.emptyList());
+
+ private final @NotNull List<PositionalParameter<?>> positionalParameters;
+
+ public Parameters(final @NotNull List<PositionalParameter<?>> positionalParameters) {
+ super();
+
+ this.positionalParameters = positionalParameters;
+
+ boolean seenOptional = false;
+ boolean seenOnlyLast = false;
+ for (final PositionalParameter<?> param : positionalParameters) {
+ final boolean isOptional = param instanceof PositionalParameter.OptionalSingle || param instanceof PositionalParameter.OptionalRemainder;
+ final boolean isOnlyLast = param instanceof PositionalParameter.RequiredRemainder || param instanceof PositionalParameter.OptionalRemainder;
+ if (seenOnlyLast) {
+ throw new IllegalArgumentException("A remainder positional parameter cannot be followed by any more positional parameters");
+ }
+ if (seenOptional && isOptional) {
+ throw new IllegalArgumentException("Required positional parameter " + param + " cannot follow an optional positional parameter");
+ }
+ seenOptional |= isOptional;
+ seenOnlyLast |= isOnlyLast;
+ }
+ }
+
+ public @NotNull List<PositionalParameter<?>> getPositionalParameters() {
+ return this.positionalParameters;
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/ParsedArguments.java b/src/main/java/de/prob2/jupyter/ParsedArguments.java
new file mode 100644
index 0000000000000000000000000000000000000000..3d8a81e85297b3af4c681a59d972cc4ed3c30045
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/ParsedArguments.java
@@ -0,0 +1,42 @@
+package de.prob2.jupyter;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import com.google.common.base.MoreObjects;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class ParsedArguments {
+ private final @NotNull Map<@NotNull Parameter<?>, Object> values;
+
+ public ParsedArguments(final @NotNull Map<@NotNull Parameter<?>, Object> values) {
+ super();
+
+ this.values = new HashMap<>(values);
+ }
+
+ public boolean containsKey(final @NotNull Parameter<?> parameter) {
+ return this.values.containsKey(parameter);
+ }
+
+ public <T> T get(final @NotNull Parameter<T> parameter) {
+ if (!this.containsKey(parameter)) {
+ throw new IllegalArgumentException("No value present for parameter " + parameter);
+ }
+ @SuppressWarnings("unchecked")
+ final T value = (T)this.values.get(parameter);
+ return value;
+ }
+
+ public <T> void put(final @NotNull Parameter<T> parameter, final T value) {
+ this.values.put(parameter, value);
+ }
+
+ @Override
+ public String toString() {
+ return MoreObjects.toStringHelper(this)
+ .add("values", this.values)
+ .toString();
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/PositionalParameter.java b/src/main/java/de/prob2/jupyter/PositionalParameter.java
new file mode 100644
index 0000000000000000000000000000000000000000..f127f49cafb75f93e004d6b671af1dca1b95cfd0
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/PositionalParameter.java
@@ -0,0 +1,98 @@
+package de.prob2.jupyter;
+
+import java.util.Optional;
+
+import org.jetbrains.annotations.NotNull;
+
+public abstract class PositionalParameter<T> extends Parameter<T> {
+ public static final class RequiredSingle extends PositionalParameter<@NotNull String> {
+ public RequiredSingle(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return false;
+ }
+
+ @Override
+ public @NotNull String getDefaultValue() {
+ throw new UnsupportedOperationException("Not an optional parameter");
+ }
+
+ @Override
+ public @NotNull Parameter.ParseResult<@NotNull String> parse(final @NotNull String argString) {
+ final String[] split = CommandUtils.ARG_SPLIT_PATTERN.split(argString, 2);
+ return new Parameter.ParseResult<>(split[0], split.length > 1 ? split[1] : "");
+ }
+ }
+
+ public static final class OptionalSingle extends PositionalParameter<@NotNull Optional<String>> {
+ public OptionalSingle(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return true;
+ }
+
+ @Override
+ public @NotNull Optional<String> getDefaultValue() {
+ return Optional.empty();
+ }
+
+ @Override
+ public @NotNull Parameter.ParseResult<@NotNull Optional<String>> parse(final @NotNull String argString) {
+ final String[] split = CommandUtils.ARG_SPLIT_PATTERN.split(argString, 2);
+ return new Parameter.ParseResult<>(Optional.of(split[0]), split.length > 1 ? split[1] : "");
+ }
+ }
+
+ public static final class RequiredRemainder extends PositionalParameter<@NotNull String> {
+ public RequiredRemainder(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return false;
+ }
+
+ @Override
+ public @NotNull String getDefaultValue() {
+ throw new UnsupportedOperationException("Not an optional parameter");
+ }
+
+ @Override
+ public Parameter.ParseResult<@NotNull String> parse(final @NotNull String argString) {
+ return new Parameter.ParseResult<>(argString, "");
+ }
+ }
+
+ public static final class OptionalRemainder extends PositionalParameter<@NotNull Optional<String>> {
+ public OptionalRemainder(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return true;
+ }
+
+ @Override
+ public @NotNull Optional<String> getDefaultValue() {
+ return Optional.empty();
+ }
+
+ @Override
+ public Parameter.ParseResult<@NotNull Optional<String>> parse(final @NotNull String argString) {
+ return new Parameter.ParseResult<>(Optional.of(argString), "");
+ }
+ }
+
+ protected PositionalParameter(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index d32646d1cb65d6132ecc0d0cc97b909dc36fe995..f126d0214f94548036ed0bf332a7d090f643b4d1 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -297,7 +297,7 @@ public final class ProBKernel extends BaseKernel {
}
final DisplayData result;
try {
- result = command.run(argString);
+ result = command.run(CommandUtils.parseArgs(command.getParameters(), argString));
} catch (final UserErrorException e) {
throw new CommandExecutionException(name, e);
}
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 0d79d7ac62b1f02ccf67a5700a7ad2adf12225fb..55574b0cbf91a053b46f035f95e7ccc373aa7860 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -9,6 +11,9 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -20,6 +25,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class AssertCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder FORMULA_PARAM = new PositionalParameter.RequiredRemainder("formula");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -36,6 +43,11 @@ public final class AssertCommand implements Command {
return ":assert";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":assert PREDICATE";
@@ -54,8 +66,8 @@ public final class AssertCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM));
final AbstractEvalResult result = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.TRUNCATE));
if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index 6ec6593be8c7687d38ebfbd72e2d362f4e700d11..28ca4af4f592ac2a5d775c85e28c6f22ba0966fc 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -11,9 +11,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.LoadedMachine;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
-
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.UserErrorException;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -38,6 +38,11 @@ public final class BrowseCommand implements Command {
return ":browse";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":browse";
@@ -58,11 +63,7 @@ public final class BrowseCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Unexpected argument: " + argString);
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final StringBuilder sb = new StringBuilder("Machine: ");
sb.append(trace.getStateSpace().getMainComponent());
diff --git a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
index 07bcee83a6a0343eb84a4175d5795924c1e1939e..e799a475c480be6557364617ddad5e80987e767a 100644
--- a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
@@ -3,6 +3,8 @@ package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -21,6 +23,11 @@ public final class BsymbCommand implements Command {
return ":bsymb";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":bsymb";
@@ -37,7 +44,7 @@ public final class BsymbCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final DisplayData data = new DisplayData("Your current environment uses plain text output; the bsymb.sty LaTeX commands will not be loaded.");
// The actual bsymb definitions are added by the ProBKernel class when it processes the command result, and the error message below will be replaced.
// If this error message is visible to the user, it means that the definitions were not added correctly.
diff --git a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
index 7f06044eecab3161f2ab11c2ce816a0f848d79f5..088dcce1a2bc911bac6c688cf24b3ea8a991358d 100644
--- a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
@@ -22,6 +22,9 @@ import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -31,6 +34,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class CheckCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle WHAT_PARAM = new PositionalParameter.RequiredSingle("what");
+
private static final @NotNull Map<@NotNull String, @NotNull Class<? extends AbstractTheoremElement>> CHILDREN_BASE_CLASS_MAP;
static {
final Map<String, Class<? extends AbstractTheoremElement>> childrenBaseClassMap = new HashMap<>();
@@ -54,6 +59,11 @@ public final class CheckCommand implements Command {
return ":check";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(WHAT_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":check WHAT";
@@ -70,11 +80,12 @@ public final class CheckCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!CHILDREN_BASE_CLASS_MAP.containsKey(argString)) {
- throw new UserErrorException("Don't know how to check " + argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String what = args.get(WHAT_PARAM);
+ if (!CHILDREN_BASE_CLASS_MAP.containsKey(what)) {
+ throw new UserErrorException("Don't know how to check " + what);
}
- final Class<? extends AbstractTheoremElement> childrenBaseClass = CHILDREN_BASE_CLASS_MAP.get(argString);
+ final Class<? extends AbstractTheoremElement> childrenBaseClass = CHILDREN_BASE_CLASS_MAP.get(what);
final Trace trace = this.animationSelector.getCurrentTrace();
// Find all children of a subclass of childrenBaseClass.
// This needs to be done manually, because getChildrenOfType only returns children whose class *exactly* matches the given class.
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 264a3fef76ac7953ccd7a9326c81bc1275d46598..1dc90cce6f547ca0bc1dc8aad7109ce4fae3a343 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -12,6 +12,9 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -21,6 +24,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ConstantsCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalRemainder PREDICATE_PARAM = new PositionalParameter.OptionalRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -37,6 +42,11 @@ public final class ConstantsCommand implements Command {
return ":constants";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":constants [PREDICATE]";
@@ -53,13 +63,13 @@ public final class ConstantsCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String predicate;
- if (argString.isEmpty()) {
+ if (!args.get(PREDICATE_PARAM).isPresent()) {
predicate = "1=1";
} else {
- predicate = this.kernelProvider.get().insertLetVariables(argString);
+ predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1);
assert !ops.isEmpty();
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index 1e10001b57aa64f40916ee43d06dd7976ab357e2..75e48d972e130cb4529689a6572ea5e5616075b8 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -4,6 +4,7 @@ import java.io.IOException;
import java.io.UncheckedIOException;
import java.nio.file.Files;
import java.nio.file.Path;
+import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;
@@ -21,6 +22,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -31,6 +35,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class DotCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle COMMAND_PARAM = new PositionalParameter.RequiredSingle("command");
+ private static final @NotNull PositionalParameter.OptionalRemainder FORMULA_PARAM = new PositionalParameter.OptionalRemainder("formula");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -47,6 +54,11 @@ public final class DotCommand implements Command {
return ":dot";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(COMMAND_PARAM, FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":dot COMMAND [FORMULA]";
@@ -76,19 +88,17 @@ public final class DotCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- assert !split.isEmpty();
- final String command = split.get(0);
- final List<IEvalElement> args;
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String command = args.get(COMMAND_PARAM);
+ final List<IEvalElement> dotCommandArgs;
final String code;
- if (split.size() > 1) {
- code = this.kernelProvider.get().insertLetVariables(split.get(1));
+ if (args.get(FORMULA_PARAM).isPresent()) {
+ code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM).get());
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND));
- args = Collections.singletonList(formula);
+ dotCommandArgs = Collections.singletonList(formula);
} else {
code = null;
- args = Collections.emptyList();
+ dotCommandArgs = Collections.emptyList();
}
final Trace trace = this.animationSelector.getCurrentTrace();
@@ -105,7 +115,7 @@ public final class DotCommand implements Command {
} catch (final IOException e) {
throw new UncheckedIOException("Failed to create temp file", e);
}
- final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), args);
+ final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), dotCommandArgs);
// Provide source code (if any) to error highlighter
final Runnable execute = () -> trace.getStateSpace().execute(cmd2);
if (code != null) {
@@ -119,7 +129,7 @@ public final class DotCommand implements Command {
} catch (final IOException e) {
throw new UncheckedIOException("Failed to read dot output", e);
}
- final DisplayData result = new DisplayData(String.format("<Dot visualization: %s %s>", command, args));
+ final DisplayData result = new DisplayData(String.format("<Dot visualization: %s %s>", command, dotCommandArgs));
result.putSVG(svg);
return result;
}
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index 74c47cf90ab4a5f1331d0341954c811245bae60c..30de5cd08f16111c5852bcaa566a1aa6006f0713 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Injector;
@@ -7,6 +9,9 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -16,6 +21,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class EvalCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder FORMULA_PARAM = new PositionalParameter.RequiredRemainder("formula");
+
private final @NotNull Injector injector;
private final @NotNull AnimationSelector animationSelector;
@@ -32,6 +39,11 @@ public final class EvalCommand implements Command {
return ":eval";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return "FORMULA\n// or\n:eval FORMULA";
@@ -49,8 +61,8 @@ public final class EvalCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String code = this.injector.getInstance(ProBKernel.class).insertLetVariables(argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String code = this.injector.getInstance(ProBKernel.class).insertLetVariables(args.get(FORMULA_PARAM));
return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.EXPAND)));
}
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 3135e0126b026a497f1cf07aab2f924de1f5f1e3..931a5ca1f68275c869fe107db37736861c3b0eb7 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -1,5 +1,6 @@
package de.prob2.jupyter.commands;
+import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;
@@ -13,6 +14,9 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -22,6 +26,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ExecCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle OPERATION_PARAM = new PositionalParameter.RequiredSingle("operation");
+ private static final @NotNull PositionalParameter.OptionalRemainder PREDICATE_PARAM = new PositionalParameter.OptionalRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -38,6 +45,11 @@ public final class ExecCommand implements Command {
return ":exec";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(OPERATION_PARAM, PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":exec OPERATION [PREDICATE]";
@@ -55,17 +67,14 @@ public final class ExecCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- assert !split.isEmpty();
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String translatedOpName = CommandUtils.unprettyOperationName(split.get(0));
+ final String translatedOpName = CommandUtils.unprettyOperationName(args.get(OPERATION_PARAM));
final String predicate;
- if (split.size() < 2) {
+ if (!args.get(PREDICATE_PARAM).isPresent()) {
predicate = "1=1";
} else {
- predicate = this.kernelProvider.get().insertLetVariables(split.get(1));
+ predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
assert !ops.isEmpty();
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index 0664e959b86ca1b0ed65eb270e1afe877ca033a8..e1aae326b416ad06dd22743d485a0dc8d6d9a829 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -9,6 +11,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -18,6 +23,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class FindCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder PREDICATE_PARAM = new PositionalParameter.RequiredRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -34,6 +41,11 @@ public final class FindCommand implements Command {
return ":find";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":find PREDICATE";
@@ -51,9 +63,9 @@ public final class FindCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM));
final Trace newTrace = CommandUtils.withSourceCode(code, () -> {
final IEvalElement pred = trace.getModel().parseFormula(code, FormulaExpand.EXPAND);
return trace.getStateSpace().getTraceToState(pred);
diff --git a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
index 14c07f32731c64d8a504fd0567cbcc17a6625fec..78770f246d78b5e71501def594846a7ef1a2f265 100644
--- a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
@@ -1,11 +1,16 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -15,6 +20,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class GotoCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle INDEX_PARAM = new PositionalParameter.RequiredSingle("index");
+
private final @NotNull AnimationSelector animationSelector;
@Inject
@@ -29,6 +36,11 @@ public final class GotoCommand implements Command {
return ":goto";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(INDEX_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":goto INDEX";
@@ -46,8 +58,8 @@ public final class GotoCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final int index = Integer.parseInt(argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final int index = Integer.parseInt(args.get(INDEX_PARAM));
final Trace trace = this.animationSelector.getCurrentTrace();
if (index < -1 || index >= trace.size()) {
throw new UserErrorException(String.format("Invalid trace index %d, must be in -1..%d", index, trace.size()-1));
diff --git a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
index ad1e99df64392316d690070c1d4a7d19f041359c..43bfe4f67b5daa8dfb97fce8484c8bd5a0570202 100644
--- a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
@@ -1,5 +1,6 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
import java.util.Objects;
import javax.script.ScriptEngine;
@@ -11,6 +12,9 @@ import com.google.inject.Injector;
import de.prob.scripting.ScriptEngineProvider;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -20,6 +24,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class GroovyCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder EXPRESSION_PARAM = new PositionalParameter.RequiredRemainder("expression");
+
private final @NotNull Injector injector;
private final @NotNull ScriptEngine groovyScriptEngine;
@@ -36,6 +42,11 @@ public final class GroovyCommand implements Command {
return ":groovy";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(EXPRESSION_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":groovy EXPRESSION";
@@ -52,11 +63,11 @@ public final class GroovyCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
this.groovyScriptEngine.put("__console", this.injector.getInstance(ProBKernel.class).getIO().out);
final Object result;
try {
- result = this.groovyScriptEngine.eval(argString);
+ result = this.groovyScriptEngine.eval(args.get(EXPRESSION_PARAM));
} catch (ScriptException e) {
throw new RuntimeException(e);
} finally {
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 5203da148a898072b781950311475b589d1d21cf..487e63a9d8c672221912f1edf3c41074fc1da2de 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -13,7 +13,9 @@ import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -24,6 +26,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class HelpCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalSingle COMMAND_NAME_PARAM = new PositionalParameter.OptionalSingle("commandName");
+
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<>();
@@ -73,6 +77,11 @@ public final class HelpCommand implements Command {
return ":help";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(COMMAND_NAME_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":help [COMMAND]";
@@ -89,10 +98,9 @@ public final class HelpCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
- final List<String> args = CommandUtils.splitArgs(argString);
- if (args.isEmpty()) {
+ if (!args.get(COMMAND_NAME_PARAM).isPresent()) {
final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\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. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n");
@@ -141,8 +149,8 @@ public final class HelpCommand implements Command {
final DisplayData result = new DisplayData(sb.toString());
result.putMarkdown(sbMarkdown.toString());
return result;
- } else if (args.size() == 1) {
- String commandName = args.get(0);
+ } else {
+ String commandName = args.get(COMMAND_NAME_PARAM).get();
// If the user entered a command name without colons, add one or two colons as appropriate.
// (If the command cannot be found, no colons are added, because we'll error out later anyway.)
if (!commandName.startsWith(":")) {
@@ -158,8 +166,6 @@ public final class HelpCommand implements Command {
throw new UserErrorException(String.format("Cannot display help for unknown command \"%s\"", commandName));
}
return command.renderHelp();
- } else {
- throw new UserErrorException("Expected at most 1 argument, got " + args.size());
}
}
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 1599a1d3e879061b0a6c9bd7c03328704c0dae56..b7bf1555d896452bd6a7559bf3e6d7c3aa1c96fa 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -12,6 +12,9 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -21,6 +24,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class InitialiseCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalRemainder PREDICATE_PARAM = new PositionalParameter.OptionalRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -37,6 +42,11 @@ public final class InitialiseCommand implements Command {
return ":init";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":init [PREDICATE]";
@@ -53,13 +63,13 @@ public final class InitialiseCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String predicate;
- if (argString.isEmpty()) {
+ if (!args.get(PREDICATE_PARAM).isPresent()) {
predicate = "1=1";
} else {
- predicate = this.kernelProvider.get().insertLetVariables(argString);
+ predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1);
assert !ops.isEmpty();
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 92332774df85f93dff0f492c6ac30414bd9266cb..4d7d6826188e007c080cd830d07e033c04c3fe71 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -1,6 +1,6 @@
package de.prob2.jupyter.commands;
-import java.util.List;
+import java.util.Arrays;
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -11,8 +11,10 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
-import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -21,6 +23,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class LetCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle NAME_PARAM = new PositionalParameter.RequiredSingle("name");
+ private static final @NotNull PositionalParameter.RequiredRemainder EXPRESSION_PARAM = new PositionalParameter.RequiredRemainder("expression");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -37,6 +42,11 @@ public final class LetCommand implements Command {
return ":let";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(NAME_PARAM, EXPRESSION_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":let NAME EXPR";
@@ -55,13 +65,9 @@ public final class LetCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- if (split.size() != 2) {
- throw new UserErrorException("Expected 2 arguments, not " + split.size());
- }
- final String name = split.get(0);
- final String expr = this.kernelProvider.get().insertLetVariables(split.get(1));
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String name = args.get(NAME_PARAM);
+ final String expr = this.kernelProvider.get().insertLetVariables(args.get(EXPRESSION_PARAM));
final AbstractEvalResult evaluated = CommandUtils.withSourceCode(expr, () -> this.animationSelector.getCurrentTrace().evalCurrent(expr, FormulaExpand.EXPAND));
if (evaluated instanceof EvalResult) {
this.kernelProvider.get().getVariables().put(name, evaluated.toString());
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index e08a3c0fb1b5ab19ce67a0dc823b7fa4c16c30c4..3f115cb5de179fae11f89ac8c5b2384a9a71a8fd 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -1,6 +1,7 @@
package de.prob2.jupyter.commands;
import java.nio.file.Paths;
+import java.util.Collections;
import java.util.List;
import java.util.Map;
@@ -12,6 +13,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -22,6 +26,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class LoadCellCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder PREFS_AND_CODE_PARAM = new PositionalParameter.RequiredRemainder("prefsAndCode");
+
private final @NotNull ClassicalBFactory classicalBFactory;
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Provider<ProBKernel> proBKernelProvider;
@@ -44,6 +50,11 @@ public final class LoadCellCommand implements Command {
return "::load";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREFS_AND_CODE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return "MACHINE\n...\nEND\n\n// or\n\n::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
@@ -62,15 +73,15 @@ public final class LoadCellCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String[] split = argString.split("\n", 2);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String[] split = args.get(PREFS_AND_CODE_PARAM).split("\n", 2);
if (split.length != 2) {
throw new UserErrorException("Missing command body");
}
final String prefsString = split[0];
final String body = split[1];
- final List<String> args = CommandUtils.splitArgs(prefsString);
- final Map<String, String> preferences = CommandUtils.parsePreferences(args);
+ final List<String> prefsSplit = CommandUtils.splitArgs(prefsString);
+ final Map<String, String> preferences = CommandUtils.parsePreferences(prefsSplit);
this.animationSelector.changeCurrentAnimation(new Trace(CommandUtils.withSourceCode(body, () ->
this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences)
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index 5d14a5de3c73f1f22eea81c8ad8e918adbc3af62..4d2155efd15607e716214ac36aef306265397a4d 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -4,6 +4,8 @@ import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
+import java.util.Arrays;
+import java.util.Collections;
import java.util.List;
import java.util.Map;
import java.util.stream.Collectors;
@@ -20,6 +22,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -34,6 +39,9 @@ import org.slf4j.LoggerFactory;
public final class LoadFileCommand implements Command {
private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(LoadFileCommand.class);
+ private static final @NotNull PositionalParameter.RequiredSingle FILE_NAME_PARAM = new PositionalParameter.RequiredSingle("fileName");
+ private static final @NotNull PositionalParameter.OptionalRemainder PREFS_PARAM = new PositionalParameter.OptionalRemainder("prefs");
+
private final @NotNull Injector injector;
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Provider<ProBKernel> proBKernelProvider;
@@ -56,6 +64,11 @@ public final class LoadFileCommand implements Command {
return ":load";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(FILE_NAME_PARAM, PREFS_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":load FILENAME [PREF=VALUE ...]";
@@ -73,13 +86,8 @@ public final class LoadFileCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> args = CommandUtils.splitArgs(argString);
- if (args.isEmpty()) {
- throw new UserErrorException("Missing machine file name");
- }
-
- final Path machineFilePath = Paths.get(args.get(0));
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final Path machineFilePath = Paths.get(args.get(FILE_NAME_PARAM));
final String machineFileName = machineFilePath.getFileName().toString();
final Path machineFileDirectory = machineFilePath.getParent() == null ? Paths.get("") : machineFilePath.getParent();
final int dotIndex = machineFileName.lastIndexOf('.');
@@ -90,7 +98,12 @@ public final class LoadFileCommand implements Command {
if (!FactoryProvider.isExtensionKnown(extension)) {
throw new UserErrorException("Unsupported file type: ." + extension);
}
- final Map<String, String> preferences = CommandUtils.parsePreferences(args.subList(1, args.size()));
+ final Map<String, String> preferences;
+ if (args.get(PREFS_PARAM).isPresent()) {
+ preferences = CommandUtils.parsePreferences(CommandUtils.splitArgs(args.get(PREFS_PARAM).get()));
+ } else {
+ preferences = Collections.emptyMap();
+ }
try {
final ModelFactory<?> factory = this.injector.getInstance(FactoryProvider.factoryClassFromExtension(extension));
diff --git a/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java b/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java
index 7356c6e89b23894ca5e2110e697ea22df110e3c1..8c45b168e80d43c306b85abb001d0e4a9c49bef4 100644
--- a/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java
@@ -16,6 +16,8 @@ import de.prob.check.StateSpaceStats;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.StateSpace;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -45,6 +47,11 @@ public final class ModelCheckCommand implements Command {
return ":modelcheck";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":modelcheck";
@@ -80,11 +87,7 @@ public final class ModelCheckCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Unexpected argument: " + argString);
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StateSpace stateSpace = this.animationSelector.getCurrentTrace().getStateSpace();
final JupyterIO io = this.kernelProvider.get().getIO();
diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
index 2be853717d8dc08dba01c75ae01808b7950103f1..89df593cd20dca25f67ea375ad1df8a8364889f4 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
@@ -1,6 +1,7 @@
package de.prob2.jupyter.commands;
import java.util.ArrayList;
+import java.util.Collections;
import java.util.List;
import java.util.TreeMap;
@@ -14,6 +15,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -23,6 +27,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class PrefCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalRemainder PREFS_PARAM = new PositionalParameter.OptionalRemainder("prefs");
+
private final @NotNull AnimationSelector animationSelector;
@Inject
@@ -37,6 +43,11 @@ public final class PrefCommand implements Command {
return ":pref";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREFS_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":pref [NAME ...]\n// or\n:pref NAME=VALUE [NAME=VALUE ...]";
@@ -54,10 +65,9 @@ public final class PrefCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> args = CommandUtils.splitArgs(argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StringBuilder sb = new StringBuilder();
- if (args.isEmpty()) {
+ if (!args.get(PREFS_PARAM).isPresent()) {
final GetCurrentPreferencesCommand cmd = new GetCurrentPreferencesCommand();
this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
// TreeMap is used to sort the preferences by name.
@@ -67,31 +77,34 @@ public final class PrefCommand implements Command {
sb.append(v);
sb.append('\n');
});
- } else if (args.get(0).contains("=")) {
- final List<SetPreferenceCommand> cmds = new ArrayList<>();
- CommandUtils.parsePreferences(args).forEach((pref, value) -> {
- cmds.add(new SetPreferenceCommand(pref, value));
- sb.append("Preference changed: ");
- sb.append(pref);
- sb.append(" = ");
- sb.append(value);
- sb.append('\n');
- });
- this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
} else {
- final List<GetPreferenceCommand> cmds = new ArrayList<>();
- for (final String arg : args) {
- if (arg.contains("=")) {
- throw new UserErrorException(String.format("Cannot view and change preferences in the same command (attempted to assign preference %s)", arg));
+ final List<String> prefsSplit = CommandUtils.splitArgs(args.get(PREFS_PARAM).get());
+ if (prefsSplit.get(0).contains("=")) {
+ final List<SetPreferenceCommand> cmds = new ArrayList<>();
+ CommandUtils.parsePreferences(prefsSplit).forEach((pref, value) -> {
+ cmds.add(new SetPreferenceCommand(pref, value));
+ sb.append("Preference changed: ");
+ sb.append(pref);
+ sb.append(" = ");
+ sb.append(value);
+ sb.append('\n');
+ });
+ this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
+ } else {
+ final List<GetPreferenceCommand> cmds = new ArrayList<>();
+ for (final String arg : prefsSplit) {
+ if (arg.contains("=")) {
+ throw new UserErrorException(String.format("Cannot view and change preferences in the same command (attempted to assign preference %s)", arg));
+ }
+ cmds.add(new GetPreferenceCommand(arg));
+ }
+ this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
+ for (final GetPreferenceCommand cmd : cmds) {
+ sb.append(cmd.getKey());
+ sb.append(" = ");
+ sb.append(cmd.getValue());
+ sb.append('\n');
}
- cmds.add(new GetPreferenceCommand(arg));
- }
- this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
- for (final GetPreferenceCommand cmd : cmds) {
- sb.append(cmd.getKey());
- sb.append(" = ");
- sb.append(cmd.getValue());
- sb.append('\n');
}
}
return new DisplayData(sb.toString());
diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
index fc0a2a257efd4dbeb44dedc5e68f3cc19f76fb58..a6fe79afe337eb2df2017c68a935788e56e1584c 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import de.prob.animator.command.PrettyPrintFormulaCommand;
@@ -8,6 +10,9 @@ import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -16,6 +21,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class PrettyPrintCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder PREDICATE_PARAM = new PositionalParameter.RequiredRemainder("predicate");
+
private final AnimationSelector animationSelector;
@Inject
@@ -30,6 +37,11 @@ public final class PrettyPrintCommand implements Command {
return ":prettyprint";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":prettyprint PREDICATE";
@@ -47,14 +59,15 @@ public final class PrettyPrintCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final IEvalElement formula = this.animationSelector.getCurrentTrace().getModel().parseFormula(argString, FormulaExpand.EXPAND);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String code = args.get(PREDICATE_PARAM);
+ final IEvalElement formula = this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND);
final PrettyPrintFormulaCommand cmdUnicode = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.UNICODE);
cmdUnicode.setOptimize(false);
final PrettyPrintFormulaCommand cmdLatex = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.LATEX);
cmdLatex.setOptimize(false);
- CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().getStateSpace().execute(cmdUnicode, cmdLatex));
+ CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getStateSpace().execute(cmdUnicode, cmdLatex));
final DisplayData ret = new DisplayData(cmdUnicode.getPrettyPrint());
ret.putLatex('$' + cmdLatex.getPrettyPrint() + '$');
diff --git a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
index 51d77d6961275e27156b94e882768f7d595fe4c3..4e3785592479efbe57ba51d6fcc805452ce26887 100644
--- a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
@@ -1,8 +1,13 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -12,6 +17,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class RenderCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder MIME_TYPE_AND_CONTENT_PARAM = new PositionalParameter.RequiredRemainder("mimeTypeAndContent");
+
@Inject
private RenderCommand() {
super();
@@ -22,6 +29,11 @@ public final class RenderCommand implements Command {
return "::render";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(MIME_TYPE_AND_CONTENT_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return "::render MIMETYPE\nCONTENT";
@@ -39,8 +51,8 @@ public final class RenderCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String[] split = argString.split("\n", 2);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String[] split = args.get(MIME_TYPE_AND_CONTENT_PARAM).split("\n", 2);
if (split.length != 2) {
throw new UserErrorException("Missing content (the content cannot be placed on the same line as the command)");
}
diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
index 592ba3786150c106aa64b1181dee92e9294b3ec9..84441d3612e742607cc4e30ef14f4f6eed8bd71c 100644
--- a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
@@ -16,6 +16,8 @@ import de.prob.animator.domainobjects.AnimationMatrixEntry;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -42,6 +44,11 @@ public final class ShowCommand implements Command {
return ":show";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":show";
@@ -58,11 +65,7 @@ public final class ShowCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Expected no arguments");
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
if (!trace.getCurrentState().isInitialised()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index f89ee34f5378666a3bd62731b3c299a16b28deba..d172344c5970dfdf5b90ef8f7ecc68a3168c37a1 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -16,6 +16,9 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -26,6 +29,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class SolveCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle SOLVER_PARAM = new PositionalParameter.RequiredSingle("solver");
+ private static final @NotNull PositionalParameter.RequiredRemainder PREDICATE_PARAM = new PositionalParameter.RequiredRemainder("predicate");
+
private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
.collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s));
@@ -45,6 +51,11 @@ public final class SolveCommand implements Command {
return ":solve";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(SOLVER_PARAM, PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":solve SOLVER PREDICATE";
@@ -67,18 +78,13 @@ public final class SolveCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- if (split.size() != 2) {
- throw new UserErrorException("Expected 2 arguments, got 1");
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final CbcSolveCommand.Solvers solver = SOLVERS.get(split.get(0));
+ final CbcSolveCommand.Solvers solver = SOLVERS.get(args.get(SOLVER_PARAM));
if (solver == null) {
- throw new UserErrorException("Unknown solver: " + split.get(0));
+ throw new UserErrorException("Unknown solver: " + args.get(SOLVER_PARAM));
}
- final String code = this.kernelProvider.get().insertLetVariables(split.get(1));
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM));
final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
diff --git a/src/main/java/de/prob2/jupyter/commands/StatsCommand.java b/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
index 212fd82609d86c3a6028b13c44935eb62e378e55..8c180dc3ebd6f9d74035aab0fd77827b6a5d2dd3 100644
--- a/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
@@ -5,9 +5,9 @@ import com.google.inject.Inject;
import de.prob.animator.command.ComputeStateSpaceStatsCommand;
import de.prob.check.StateSpaceStats;
import de.prob.statespace.AnimationSelector;
-
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.UserErrorException;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -30,6 +30,11 @@ public final class StatsCommand implements Command {
return ":stats";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":stats";
@@ -46,10 +51,7 @@ public final class StatsCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Expected no arguments");
- }
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ComputeStateSpaceStatsCommand cmd = new ComputeStateSpaceStatsCommand();
this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
final StateSpaceStats stats = cmd.getResult();
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index 9a4e3a8800a8066ae469baca0f8b63ab75603db3..c43bb8c83564671f15739665d34de1f74e9afd0b 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
@@ -18,6 +18,9 @@ import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -27,6 +30,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TableCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder EXPRESSION_PARAM = new PositionalParameter.RequiredRemainder("expression");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -43,6 +48,11 @@ public final class TableCommand implements Command {
return ":table";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(EXPRESSION_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":table EXPRESSION";
@@ -59,9 +69,9 @@ public final class TableCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(EXPRESSION_PARAM));
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final GetAllTableCommands cmd1 = new GetAllTableCommands(trace.getCurrentState());
diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
index ac426637127262327d04e4882a3b2a72bb0f7deb..aacd756df8ccb57d3805be0d45567c96c983018b 100644
--- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
@@ -2,12 +2,16 @@ package de.prob2.jupyter.commands;
import java.time.Duration;
import java.time.temporal.ChronoUnit;
+import java.util.Collections;
import com.google.common.base.Stopwatch;
import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -17,6 +21,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TimeCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder COMMAND_AND_ARGS_PARAM = new PositionalParameter.RequiredRemainder("commandAndArgs");
+
private final @NotNull Injector injector;
@Inject
@@ -31,6 +37,11 @@ public final class TimeCommand implements Command {
return ":time";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(COMMAND_AND_ARGS_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":time COMMAND [ARGS ...]";
@@ -48,10 +59,10 @@ public final class TimeCommand implements Command {
}
@Override
- public @Nullable DisplayData run(final @NotNull String argString) {
+ public @Nullable DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
final Stopwatch stopwatch = Stopwatch.createStarted();
- final DisplayData result = kernel.eval(argString);
+ final DisplayData result = kernel.eval(args.get(COMMAND_AND_ARGS_PARAM));
stopwatch.stop();
final Duration elapsed = stopwatch.elapsed();
final String text = String.format("Execution time: %d.%09d seconds", elapsed.get(ChronoUnit.SECONDS), elapsed.get(ChronoUnit.NANOS));
diff --git a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
index 2cb417c9031cbcb72b52f06d7b6990d18d4307d2..b37af724e9cf22c59eb7ec66b28bd8558db21c93 100644
--- a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
@@ -7,9 +7,9 @@ import com.google.inject.Inject;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
-
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.UserErrorException;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -32,6 +32,11 @@ public final class TraceCommand implements Command {
return ":trace";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":trace";
@@ -49,11 +54,7 @@ public final class TraceCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Expected no arguments");
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final StringBuilder sbPlain = new StringBuilder("-1: Root state");
final StringBuilder sbMarkdown = new StringBuilder("* -1: Root state");
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 8c900cffebe4285d854c3783a9e7d315856ac213..d8a9236dfc393379584514b24f3ad5b4c240e302 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -11,6 +13,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -20,6 +25,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TypeCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder FORMULA_PARAM = new PositionalParameter.RequiredRemainder("formula");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -36,6 +43,11 @@ public final class TypeCommand implements Command {
return ":type";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":type FORMULA";
@@ -52,9 +64,9 @@ public final class TypeCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM));
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
if (result.isOk()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/UnletCommand.java b/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
index b2f7f1e37976d890cea1ac7bd6a9828c3950edb2..f3da397f8590a5a8e877664b66b728a4226cf140 100644
--- a/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
@@ -1,11 +1,15 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
import java.util.Map;
import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -16,6 +20,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class UnletCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle NAME_PARAM = new PositionalParameter.RequiredSingle("name");
+
private final @NotNull Injector injector;
@Inject
@@ -30,6 +36,11 @@ public final class UnletCommand implements Command {
return ":unlet";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(NAME_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":unlet NAME";
@@ -46,12 +57,13 @@ public final class UnletCommand implements Command {
}
@Override
- public @Nullable DisplayData run(final @NotNull String argString) {
+ public @Nullable DisplayData run(final @NotNull ParsedArguments args) {
final Map<String, String> variables = this.injector.getInstance(ProBKernel.class).getVariables();
- if (!variables.containsKey(argString)) {
- throw new UserErrorException("There is no local variable " + argString);
+ final String name = args.get(NAME_PARAM);
+ if (!variables.containsKey(name)) {
+ throw new UserErrorException("There is no local variable " + name);
}
- variables.remove(argString);
+ variables.remove(name);
return null;
}
diff --git a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
index c22c7f04d149e6d0b65dc868380080818ccb9cfc..d900dba62ec528c9898b3f5b6761d2f4c598861d 100644
--- a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
@@ -6,6 +6,8 @@ import de.prob.Main;
import de.prob.animator.command.GetVersionCommand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -29,6 +31,11 @@ public final class VersionCommand implements Command {
return ":version";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":version";
@@ -45,7 +52,7 @@ public final class VersionCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StringBuilder sb = new StringBuilder("ProB 2 Jupyter kernel: ");
sb.append(ProBKernel.getVersion());
sb.append(" (");