diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 28d8ca71f4c003bd65e1fa5b3eadb2a81410231f..b9422585d7d610489bec3910bc75eb45057a9ba4 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -23,6 +23,7 @@ import de.prob2.jupyter.commands.AssertCommand;
import de.prob2.jupyter.commands.BrowseCommand;
import de.prob2.jupyter.commands.Command;
import de.prob2.jupyter.commands.CommandExecutionException;
+import de.prob2.jupyter.commands.CommandUtils;
import de.prob2.jupyter.commands.ConstantsCommand;
import de.prob2.jupyter.commands.EvalCommand;
import de.prob2.jupyter.commands.ExecCommand;
@@ -240,11 +241,7 @@ public final class ProBKernel extends BaseKernel {
final String argString = commandMatcher.group(2) == null ? "" : commandMatcher.group(2);
if (this.getCommands().containsKey(name)) {
final ReplacementOptions replacements = this.getCommands().get(name).complete(this, argString, at - argOffset);
- return replacements == null ? null : new ReplacementOptions(
- replacements.getReplacements(),
- replacements.getSourceStart() + argOffset,
- replacements.getSourceEnd() + argOffset
- );
+ return replacements == null ? null : CommandUtils.offsetReplacementOptions(replacements, argOffset);
} else {
// Invalid command, can't provide any completions.
return null;
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index d78e3ab46255d1d293eddf9defd64ea1f110e0e5..7c311174aab0b8c92f51ff5473f2f561dea3ba8b 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -10,6 +10,7 @@ import de.prob.statespace.AnimationSelector;
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;
import io.github.spencerpark.jupyter.kernel.display.mime.MIMEType;
@@ -51,4 +52,9 @@ public final class AssertCommand implements Command {
}
throw new UserErrorException("Assertion is not true: " + displayData.getData(MIMEType.TEXT_PLAIN));
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
index ab57f2059bb07d98db9a8e43dd9c0d224e4eddc8..4aa1ffc979496833d622536a0779acb1b3a0c791 100644
--- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
@@ -33,6 +33,7 @@ import org.slf4j.LoggerFactory;
public final class CommandUtils {
private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(CommandUtils.class);
+ public static final @NotNull Pattern ARG_SPLIT_PATTERN = Pattern.compile("\\h+");
private static final @NotNull Pattern B_IDENTIFIER_PATTERN = Pattern.compile("[A-Za-z][A-Za-z0-9_]*");
private CommandUtils() {
@@ -41,8 +42,34 @@ public final class CommandUtils {
throw new AssertionError("Utility class");
}
+ public static @NotNull String prettyOperationName(final @NotNull String name) {
+ switch (name) {
+ case "$setup_constants":
+ return "SETUP_CONSTANTS";
+
+ case "$initialise_machine":
+ return "INITIALISATION";
+
+ default:
+ return name;
+ }
+ }
+
+ public static @NotNull String unprettyOperationName(final @NotNull String name) {
+ switch (name) {
+ case "SETUP_CONSTANTS":
+ return "$setup_constants";
+
+ case "INITIALISATION":
+ return "$initialise_machine";
+
+ default:
+ return name;
+ }
+ }
+
public static @NotNull List<@NotNull String> splitArgs(final @NotNull String args, final int limit) {
- final String[] split = args.split("\\h+", limit);
+ final String[] split = ARG_SPLIT_PATTERN.split(args, limit);
if (split.length == 1 && split[0].isEmpty()) {
return Collections.emptyList();
} else {
@@ -127,6 +154,14 @@ public final class CommandUtils {
}
}
+ public static @NotNull ReplacementOptions offsetReplacementOptions(final @NotNull ReplacementOptions replacements, final int offset) {
+ return new ReplacementOptions(
+ replacements.getReplacements(),
+ replacements.getSourceStart() + offset,
+ replacements.getSourceEnd() + offset
+ );
+ }
+
public static @NotNull ReplacementOptions completeInBExpression(final @NotNull Trace trace, final @NotNull String code, final int at) {
final Matcher identifierMatcher = B_IDENTIFIER_PATTERN.matcher(code);
String identifier = "";
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index d12caaef450ff3a0f79b3df2ebd11a10f5e7973d..2535c0dd616df4c885edbf8952c9f775c32fbca0 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -13,6 +13,7 @@ import de.prob.statespace.Transition;
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;
import org.jetbrains.annotations.NotNull;
@@ -55,4 +56,9 @@ public final class ConstantsCommand implements Command {
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Machine constants set up using operation %s: %s", op.getId(), op.getRep()));
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 286c4e96421fe17f731d6f93b42846f131310240..31774a1e89d4e48f5331e0c2052c4322d8e65f13 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -3,6 +3,9 @@ package de.prob2.jupyter.commands;
import java.util.Collections;
import java.util.List;
import java.util.Optional;
+import java.util.regex.Matcher;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
import com.google.inject.Inject;
@@ -14,6 +17,7 @@ import de.prob.statespace.Transition;
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;
import org.jetbrains.annotations.NotNull;
@@ -56,14 +60,7 @@ public final class ExecCommand implements Command {
op = opt.get();
} else {
// Transition not found, assume that the argument is an operation name instead.
- final String translatedOpName;
- if ("SETUP_CONSTANTS".equals(opNameOrId)) {
- translatedOpName = "$setup_constants";
- } else if ("INITIALISATION".equals(opNameOrId)) {
- translatedOpName = "$initialise_machine";
- } else {
- translatedOpName = opNameOrId;
- }
+ final String translatedOpName = CommandUtils.unprettyOperationName(opNameOrId);
final List<String> predicates = split.size() < 2 ? Collections.emptyList() : Collections.singletonList(split.get(1));
op = trace.getCurrentState().findTransition(translatedOpName, predicates);
if (op == null) {
@@ -75,4 +72,33 @@ public final class ExecCommand implements Command {
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Executed operation %s: %s", op.getId(), op.getRep()));
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ final int opNameEnd;
+ final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
+ if (argSplitMatcher.find()) {
+ opNameEnd = argSplitMatcher.start();
+ } else {
+ opNameEnd = argString.length();
+ }
+
+ if (opNameEnd < at) {
+ // Cursor is in the predicate part of the arguments, provide B completions.
+ final ReplacementOptions replacements = CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString.substring(opNameEnd), at - opNameEnd);
+ return CommandUtils.offsetReplacementOptions(replacements, opNameEnd);
+ } else {
+ // Cursor is in the first part of the arguments, provide possible operation names and transition IDs.
+ final String prefix = argString.substring(0, at);
+ final List<String> opNames = this.animationSelector.getCurrentTrace()
+ .getNextTransitions()
+ .stream()
+ .flatMap(t -> Stream.of(CommandUtils.prettyOperationName(t.getName()), t.getId()))
+ .distinct()
+ .filter(s -> s.startsWith(prefix))
+ .sorted()
+ .collect(Collectors.toList());
+ return new ReplacementOptions(opNames, 0, opNameEnd);
+ }
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 52fe6e734b968dfcdc93ebf22cbac7b144746a47..b2e94e5d05ac1862e7410e5c03e05b9910059192 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -13,6 +13,7 @@ import de.prob.statespace.Transition;
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;
import org.jetbrains.annotations.NotNull;
@@ -55,4 +56,9 @@ public final class InitialiseCommand implements Command {
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep()));
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
index e57886376cf02abc3c1d812e663f47ef1aa4992c..6d5a6442c454c4d0c40c205a119c63a8f6938adc 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
@@ -9,6 +9,7 @@ import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel;
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
@@ -47,4 +48,9 @@ public final class PrettyPrintCommand implements Command {
ret.putLatex('$' + cmdLatex.getPrettyPrint() + '$');
return ret;
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index 174f052b5ae1fbb69cc4ef246156072e6e2bddd8..f4b2d960bc48db89e45f3e661206714c39c9638c 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -1,6 +1,9 @@
package de.prob2.jupyter.commands;
import java.util.List;
+import java.util.regex.Matcher;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
import com.google.inject.Inject;
@@ -13,6 +16,7 @@ import de.prob.statespace.Trace;
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;
import org.jetbrains.annotations.NotNull;
@@ -76,4 +80,29 @@ public final class SolveCommand implements Command {
trace.getStateSpace().execute(cmd);
return CommandUtils.displayDataForEvalResult(cmd.getValue());
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ final int solverNameEnd;
+ final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
+ if (argSplitMatcher.find()) {
+ solverNameEnd = argSplitMatcher.start();
+ } else {
+ solverNameEnd = argString.length();
+ }
+
+ if (solverNameEnd < at) {
+ // Cursor is in the predicate part of the arguments, provide B completions.
+ final ReplacementOptions replacements = CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString.substring(solverNameEnd), at - solverNameEnd);
+ return CommandUtils.offsetReplacementOptions(replacements, solverNameEnd);
+ } else {
+ // Cursor is in the solver name.
+ final String prefix = argString.substring(0, at);
+ final List<String> solverNames = Stream.of("prob", "kodkod", "smt_supported_interpreter", "z3", "cvc4")
+ .filter(s -> s.startsWith(prefix))
+ .sorted()
+ .collect(Collectors.toList());
+ return new ReplacementOptions(solverNames, 0, solverNameEnd);
+ }
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index 6f0c95a5158ec1c46a325b7db4f0e6a552f2d7f3..0d22227c1528240158861493f1bf0aa330da7b18 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
@@ -16,6 +16,7 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
@@ -80,4 +81,9 @@ public final class TableCommand implements Command {
res.putMarkdown(sbMarkdown.toString());
return res;
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 2eb29f8bb11f310bb61d48564bd2ad2f22b4b20d..13167c49805e0b5392f0d47c4789abd7810c584e 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -11,6 +11,7 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
@@ -46,4 +47,9 @@ public final class TypeCommand implements Command {
throw new ProBError("Type errors in formula", result.getErrors());
}
}
+
+ @Override
+ public @NotNull ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}