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

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.
parent 3b922bfd
Branches
Tags
No related merge requests found
Showing with 137 additions and 14 deletions
...@@ -23,6 +23,7 @@ import de.prob2.jupyter.commands.AssertCommand; ...@@ -23,6 +23,7 @@ import de.prob2.jupyter.commands.AssertCommand;
import de.prob2.jupyter.commands.BrowseCommand; import de.prob2.jupyter.commands.BrowseCommand;
import de.prob2.jupyter.commands.Command; import de.prob2.jupyter.commands.Command;
import de.prob2.jupyter.commands.CommandExecutionException; import de.prob2.jupyter.commands.CommandExecutionException;
import de.prob2.jupyter.commands.CommandUtils;
import de.prob2.jupyter.commands.ConstantsCommand; import de.prob2.jupyter.commands.ConstantsCommand;
import de.prob2.jupyter.commands.EvalCommand; import de.prob2.jupyter.commands.EvalCommand;
import de.prob2.jupyter.commands.ExecCommand; import de.prob2.jupyter.commands.ExecCommand;
...@@ -240,11 +241,7 @@ public final class ProBKernel extends BaseKernel { ...@@ -240,11 +241,7 @@ public final class ProBKernel extends BaseKernel {
final String argString = commandMatcher.group(2) == null ? "" : commandMatcher.group(2); final String argString = commandMatcher.group(2) == null ? "" : commandMatcher.group(2);
if (this.getCommands().containsKey(name)) { if (this.getCommands().containsKey(name)) {
final ReplacementOptions replacements = this.getCommands().get(name).complete(this, argString, at - argOffset); final ReplacementOptions replacements = this.getCommands().get(name).complete(this, argString, at - argOffset);
return replacements == null ? null : new ReplacementOptions( return replacements == null ? null : CommandUtils.offsetReplacementOptions(replacements, argOffset);
replacements.getReplacements(),
replacements.getSourceStart() + argOffset,
replacements.getSourceEnd() + argOffset
);
} else { } else {
// Invalid command, can't provide any completions. // Invalid command, can't provide any completions.
return null; return null;
......
...@@ -10,6 +10,7 @@ import de.prob.statespace.AnimationSelector; ...@@ -10,6 +10,7 @@ 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 io.github.spencerpark.jupyter.kernel.display.mime.MIMEType; import io.github.spencerpark.jupyter.kernel.display.mime.MIMEType;
...@@ -51,4 +52,9 @@ public final class AssertCommand implements Command { ...@@ -51,4 +52,9 @@ public final class AssertCommand implements Command {
} }
throw new UserErrorException("Assertion is not true: " + displayData.getData(MIMEType.TEXT_PLAIN)); 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);
}
} }
...@@ -33,6 +33,7 @@ import org.slf4j.LoggerFactory; ...@@ -33,6 +33,7 @@ import org.slf4j.LoggerFactory;
public final class CommandUtils { public final class CommandUtils {
private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(CommandUtils.class); 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 static final @NotNull Pattern B_IDENTIFIER_PATTERN = Pattern.compile("[A-Za-z][A-Za-z0-9_]*");
private CommandUtils() { private CommandUtils() {
...@@ -41,8 +42,34 @@ public final class CommandUtils { ...@@ -41,8 +42,34 @@ public final class CommandUtils {
throw new AssertionError("Utility class"); 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) { 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()) { if (split.length == 1 && split[0].isEmpty()) {
return Collections.emptyList(); return Collections.emptyList();
} else { } else {
...@@ -127,6 +154,14 @@ public final class CommandUtils { ...@@ -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) { public static @NotNull ReplacementOptions completeInBExpression(final @NotNull Trace trace, final @NotNull String code, final int at) {
final Matcher identifierMatcher = B_IDENTIFIER_PATTERN.matcher(code); final Matcher identifierMatcher = B_IDENTIFIER_PATTERN.matcher(code);
String identifier = ""; String identifier = "";
......
...@@ -13,6 +13,7 @@ import de.prob.statespace.Transition; ...@@ -13,6 +13,7 @@ import de.prob.statespace.Transition;
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;
...@@ -55,4 +56,9 @@ public final class ConstantsCommand implements Command { ...@@ -55,4 +56,9 @@ public final class ConstantsCommand implements Command {
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); 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())); 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);
}
} }
...@@ -3,6 +3,9 @@ package de.prob2.jupyter.commands; ...@@ -3,6 +3,9 @@ package de.prob2.jupyter.commands;
import java.util.Collections; import java.util.Collections;
import java.util.List; import java.util.List;
import java.util.Optional; import java.util.Optional;
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,6 +17,7 @@ import de.prob.statespace.Transition; ...@@ -14,6 +17,7 @@ import de.prob.statespace.Transition;
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;
...@@ -56,14 +60,7 @@ public final class ExecCommand implements Command { ...@@ -56,14 +60,7 @@ public final class ExecCommand implements Command {
op = opt.get(); op = opt.get();
} else { } else {
// Transition not found, assume that the argument is an operation name instead. // Transition not found, assume that the argument is an operation name instead.
final String translatedOpName; final String translatedOpName = CommandUtils.unprettyOperationName(opNameOrId);
if ("SETUP_CONSTANTS".equals(opNameOrId)) {
translatedOpName = "$setup_constants";
} else if ("INITIALISATION".equals(opNameOrId)) {
translatedOpName = "$initialise_machine";
} else {
translatedOpName = opNameOrId;
}
final List<String> predicates = split.size() < 2 ? Collections.emptyList() : Collections.singletonList(split.get(1)); final List<String> predicates = split.size() < 2 ? Collections.emptyList() : Collections.singletonList(split.get(1));
op = trace.getCurrentState().findTransition(translatedOpName, predicates); op = trace.getCurrentState().findTransition(translatedOpName, predicates);
if (op == null) { if (op == null) {
...@@ -75,4 +72,33 @@ public final class ExecCommand implements Command { ...@@ -75,4 +72,33 @@ public final class ExecCommand implements Command {
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Executed operation %s: %s", op.getId(), op.getRep())); 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);
}
}
} }
...@@ -13,6 +13,7 @@ import de.prob.statespace.Transition; ...@@ -13,6 +13,7 @@ import de.prob.statespace.Transition;
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;
...@@ -55,4 +56,9 @@ public final class InitialiseCommand implements Command { ...@@ -55,4 +56,9 @@ public final class InitialiseCommand implements Command {
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep())); 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);
}
} }
...@@ -9,6 +9,7 @@ import de.prob.statespace.AnimationSelector; ...@@ -9,6 +9,7 @@ import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel; import de.prob2.jupyter.ProBKernel;
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;
...@@ -47,4 +48,9 @@ public final class PrettyPrintCommand implements Command { ...@@ -47,4 +48,9 @@ public final class PrettyPrintCommand implements Command {
ret.putLatex('$' + cmdLatex.getPrettyPrint() + '$'); ret.putLatex('$' + cmdLatex.getPrettyPrint() + '$');
return ret; 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);
}
} }
package de.prob2.jupyter.commands; package de.prob2.jupyter.commands;
import java.util.List; import java.util.List;
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;
...@@ -13,6 +16,7 @@ import de.prob.statespace.Trace; ...@@ -13,6 +16,7 @@ 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;
...@@ -76,4 +80,29 @@ public final class SolveCommand implements Command { ...@@ -76,4 +80,29 @@ public final class SolveCommand implements Command {
trace.getStateSpace().execute(cmd); trace.getStateSpace().execute(cmd);
return CommandUtils.displayDataForEvalResult(cmd.getValue()); 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);
}
}
} }
...@@ -16,6 +16,7 @@ import de.prob.statespace.Trace; ...@@ -16,6 +16,7 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel; import de.prob2.jupyter.ProBKernel;
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;
...@@ -80,4 +81,9 @@ public final class TableCommand implements Command { ...@@ -80,4 +81,9 @@ public final class TableCommand implements Command {
res.putMarkdown(sbMarkdown.toString()); res.putMarkdown(sbMarkdown.toString());
return res; 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);
}
} }
...@@ -11,6 +11,7 @@ import de.prob.statespace.Trace; ...@@ -11,6 +11,7 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel; import de.prob2.jupyter.ProBKernel;
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;
...@@ -46,4 +47,9 @@ public final class TypeCommand implements Command { ...@@ -46,4 +47,9 @@ public final class TypeCommand implements Command {
throw new ProBError("Type errors in formula", result.getErrors()); 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);
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment