diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
index 4aa1ffc979496833d622536a0779acb1b3a0c791..28cce18ee2f110a933a7a71f01ea6085cbef3563 100644
--- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
@@ -10,8 +10,10 @@ import java.util.Map;
import java.util.Set;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
+import java.util.stream.Collectors;
import de.prob.animator.command.CompleteIdentifierCommand;
+import de.prob.animator.command.GetCurrentPreferencesCommand;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.ComputationNotCompletedResult;
import de.prob.animator.domainobjects.EnumerationWarning;
@@ -26,6 +28,7 @@ import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
@@ -192,4 +195,23 @@ public final class CommandUtils {
return new ReplacementOptions(new ArrayList<>(completions), start, end);
}
+
+ public static @Nullable ReplacementOptions completeInPreferences(final @NotNull Trace trace, final @NotNull String code, final int at) {
+ final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(code);
+ int prefNameStart = 0;
+ while (argSplitMatcher.find() && argSplitMatcher.end() <= at) {
+ prefNameStart = argSplitMatcher.end();
+ }
+ final Matcher prefNameMatcher = B_IDENTIFIER_PATTERN.matcher(code);
+ prefNameMatcher.region(prefNameStart, code.length());
+ if (prefNameMatcher.lookingAt() && at <= prefNameMatcher.end()) {
+ final String prefix = code.substring(prefNameMatcher.start(), at);
+ final GetCurrentPreferencesCommand cmd = new GetCurrentPreferencesCommand();
+ trace.getStateSpace().execute(cmd);
+ final List<String> prefs = cmd.getPreferences().keySet().stream().filter(s -> s.startsWith(prefix)).sorted().collect(Collectors.toList());
+ return new ReplacementOptions(prefs, prefNameMatcher.start(), prefNameMatcher.end());
+ } else {
+ return null;
+ }
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index ff2cae4096e9424909f74778e68a9647ee6592c2..19b5c525fd1508110587710a20d90927870cf319 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -12,9 +12,11 @@ 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;
+import org.jetbrains.annotations.Nullable;
public final class LoadCellCommand implements Command {
private final @NotNull ClassicalBFactory classicalBFactory;
@@ -52,4 +54,16 @@ public final class LoadCellCommand implements Command {
this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create(body).load(preferences)));
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getModel());
}
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ final int newlinePos = argString.indexOf('\n');
+ if (newlinePos == -1 || at < newlinePos) {
+ // Cursor is on the first line, provide preference name completions.
+ return CommandUtils.completeInPreferences(this.animationSelector.getCurrentTrace(), argString, at);
+ } else {
+ // Cursor is in the body, provide B completions.
+ return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+ }
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index 2a4d7c61c2e6417487d7c16f6b95ae95e980da20..e1c93abfb7d5f63db92f2ca4334db5926f7b72c2 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -1,8 +1,14 @@
package de.prob2.jupyter.commands;
import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
import java.util.List;
import java.util.Map;
+import java.util.regex.Matcher;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
import com.google.inject.Inject;
@@ -14,11 +20,18 @@ 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;
+import org.jetbrains.annotations.Nullable;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
public final class LoadFileCommand implements Command {
+ private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(LoadFileCommand.class);
+
private final @NotNull ClassicalBFactory classicalBFactory;
private final @NotNull AnimationSelector animationSelector;
@@ -57,4 +70,36 @@ public final class LoadFileCommand implements Command {
}
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getModel());
}
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ final int fileNameEnd;
+ final Matcher argSplitMatcher = CommandUtils.ARG_SPLIT_PATTERN.matcher(argString);
+ if (argSplitMatcher.find()) {
+ fileNameEnd = argSplitMatcher.start();
+ } else {
+ fileNameEnd = argString.length();
+ }
+
+ if (fileNameEnd < at) {
+ // Cursor is in the preferences, provide preference name completions.
+ final ReplacementOptions replacements = CommandUtils.completeInPreferences(this.animationSelector.getCurrentTrace(), argString.substring(fileNameEnd), at - fileNameEnd);
+ return replacements == null ? null : CommandUtils.offsetReplacementOptions(replacements, fileNameEnd);
+ } else {
+ // Cursor is in the file name, provide machine files from the current directory as completions.
+ final String prefix = argString.substring(0, at);
+ final List<String> fileNames;
+ try (final Stream<Path> list = Files.list(Paths.get(""))) {
+ fileNames = list
+ .map(Path::getFileName)
+ .map(Object::toString)
+ .filter(s -> s.startsWith(prefix) && (s.endsWith(".mch") || s.endsWith(".ref") || s.endsWith(".imp")))
+ .collect(Collectors.toList());
+ } catch (final IOException e) {
+ LOGGER.warn("Could not list contents of the current directory, cannot provide file name completions for :load", e);
+ return null;
+ }
+ return new ReplacementOptions(fileNames, 0, fileNameEnd);
+ }
+ }
}
diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
index f8885d11df641dfe478c3efa519ca9b186822ed9..43d9bcb2be9815bcbbf9027958ad002aa9da58da 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
@@ -15,9 +15,11 @@ 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 org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
public final class PrefCommand implements Command {
private final @NotNull AnimationSelector animationSelector;
@@ -82,4 +84,9 @@ public final class PrefCommand implements Command {
}
return new DisplayData(sb.toString());
}
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull ProBKernel kernel, final @NotNull String argString, final int at) {
+ return CommandUtils.completeInPreferences(this.animationSelector.getCurrentTrace(), argString, at);
+ }
}