From e2b97144bbb22ccb95e33f284a2e45400c5f8a84 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 20 Jun 2018 19:14:04 +0200
Subject: [PATCH] Add code completion support to most commands
Still missing are ::load and :pref.
::render, :groovy and :load are also missing, but implementing code
completion there is probably not worth the effort.
---
.../java/de/prob2/jupyter/ProBKernel.java | 7 +---
.../prob2/jupyter/commands/AssertCommand.java | 6 +++
.../prob2/jupyter/commands/CommandUtils.java | 37 +++++++++++++++-
.../jupyter/commands/ConstantsCommand.java | 6 +++
.../prob2/jupyter/commands/ExecCommand.java | 42 +++++++++++++++----
.../jupyter/commands/InitialiseCommand.java | 6 +++
.../jupyter/commands/PrettyPrintCommand.java | 6 +++
.../prob2/jupyter/commands/SolveCommand.java | 29 +++++++++++++
.../prob2/jupyter/commands/TableCommand.java | 6 +++
.../prob2/jupyter/commands/TypeCommand.java | 6 +++
10 files changed, 137 insertions(+), 14 deletions(-)
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 28d8ca7..b942258 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 d78e3ab..7c31117 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 ab57f20..4aa1ffc 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 d12caae..2535c0d 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 286c4e9..31774a1 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 52fe6e7..b2e94e5 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 e578863..6d5a644 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 174f052..f4b2d96 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 6f0c95a..0d22227 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 2eb29f8..13167c4 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);
+ }
}
--
GitLab