Skip to content
Snippets Groups Projects
Commit 2fe24726 authored by dgelessus's avatar dgelessus
Browse files

Add code completion support to ::load, :load, and :pref

parent b685b031
No related branches found
No related tags found
No related merge requests found
...@@ -10,8 +10,10 @@ import java.util.Map; ...@@ -10,8 +10,10 @@ import java.util.Map;
import java.util.Set; import java.util.Set;
import java.util.regex.Matcher; import java.util.regex.Matcher;
import java.util.regex.Pattern; import java.util.regex.Pattern;
import java.util.stream.Collectors;
import de.prob.animator.command.CompleteIdentifierCommand; import de.prob.animator.command.CompleteIdentifierCommand;
import de.prob.animator.command.GetCurrentPreferencesCommand;
import de.prob.animator.domainobjects.AbstractEvalResult; import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.ComputationNotCompletedResult; import de.prob.animator.domainobjects.ComputationNotCompletedResult;
import de.prob.animator.domainobjects.EnumerationWarning; import de.prob.animator.domainobjects.EnumerationWarning;
...@@ -26,6 +28,7 @@ import io.github.spencerpark.jupyter.kernel.ReplacementOptions; ...@@ -26,6 +28,7 @@ import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData; import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
import org.slf4j.Logger; import org.slf4j.Logger;
import org.slf4j.LoggerFactory; import org.slf4j.LoggerFactory;
...@@ -192,4 +195,23 @@ public final class CommandUtils { ...@@ -192,4 +195,23 @@ public final class CommandUtils {
return new ReplacementOptions(new ArrayList<>(completions), start, end); 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;
}
}
} }
...@@ -12,9 +12,11 @@ import de.prob.statespace.Trace; ...@@ -12,9 +12,11 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel; import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException; 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.DisplayData;
import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class LoadCellCommand implements Command { public final class LoadCellCommand implements Command {
private final @NotNull ClassicalBFactory classicalBFactory; private final @NotNull ClassicalBFactory classicalBFactory;
...@@ -52,4 +54,16 @@ public final class LoadCellCommand implements Command { ...@@ -52,4 +54,16 @@ public final class LoadCellCommand implements Command {
this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create(body).load(preferences))); this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create(body).load(preferences)));
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getModel()); 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);
}
}
} }
package de.prob2.jupyter.commands; package de.prob2.jupyter.commands;
import java.io.IOException; 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.List;
import java.util.Map; import java.util.Map;
import java.util.regex.Matcher;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import com.google.inject.Inject; import com.google.inject.Inject;
...@@ -14,11 +20,18 @@ import de.prob.statespace.Trace; ...@@ -14,11 +20,18 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel; import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException; 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.DisplayData;
import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
public final class LoadFileCommand implements Command { public final class LoadFileCommand implements Command {
private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(LoadFileCommand.class);
private final @NotNull ClassicalBFactory classicalBFactory; private final @NotNull ClassicalBFactory classicalBFactory;
private final @NotNull AnimationSelector animationSelector; private final @NotNull AnimationSelector animationSelector;
...@@ -57,4 +70,36 @@ public final class LoadFileCommand implements Command { ...@@ -57,4 +70,36 @@ public final class LoadFileCommand implements Command {
} }
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getModel()); 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);
}
}
} }
...@@ -15,9 +15,11 @@ import de.prob.statespace.AnimationSelector; ...@@ -15,9 +15,11 @@ import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel; import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException; 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.DisplayData;
import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class PrefCommand implements Command { public final class PrefCommand implements Command {
private final @NotNull AnimationSelector animationSelector; private final @NotNull AnimationSelector animationSelector;
...@@ -82,4 +84,9 @@ public final class PrefCommand implements Command { ...@@ -82,4 +84,9 @@ public final class PrefCommand implements Command {
} }
return new DisplayData(sb.toString()); 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);
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment