CHANGELOG.md

@@ -2,7 +2,7 @@
 
 ## [(next version)](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.4.2-SNAPSHOT-all.jar?job=test)
 
-* Updated to ProB 1.13.0 (ProB Java API version 4.13.1).
+* Updated to ProB 1.15.0 (ProB Java API version 4.13.2-SNAPSHOT).
 
 ## [1.4.1](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.1-all.jar)
 

build.gradle

@@ -5,7 +5,7 @@ plugins {
 	id("java")
 	id("wrapper")
 	
-	id("com.github.johnrengelman.shadow").version("8.1.1")
+	id("com.gradleup.shadow").version("8.3.6")
 }
 
 version = "1.4.2-SNAPSHOT"
@@ -18,8 +18,8 @@ repositories {
 	mavenCentral()
 	if (isSnapshot) {
 		maven {
-			name("Sonatype snapshots")
-			url("https://oss.sonatype.org/content/repositories/snapshots")
+			name = "Sonatype snapshots"
+			url = "https://oss.sonatype.org/content/repositories/snapshots"
 		}
 	}
 }
@@ -31,12 +31,12 @@ configurations.all {
 }
 
 dependencies {
-	implementation(group: "ch.qos.logback", name: "logback-classic", version: "1.3.7")
-	implementation(group: "com.google.guava", name: "guava", version: "31.1-jre")
+	implementation(group: "ch.qos.logback", name: "logback-classic", version: "1.3.15")
+	implementation(group: "com.google.guava", name: "guava", version: "33.4.0-jre")
 	implementation(platform(group: "de.hhu.stups", name: "prob-java-bom", version: "4.13.2-SNAPSHOT"))
 	implementation(group: "de.hhu.stups", name: "de.prob2.kernel")
 	implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
-	implementation(group: "org.jetbrains", name: "annotations", version: "24.0.1")
+	implementation(group: "org.jetbrains", name: "annotations", version: "26.0.2")
 	implementation(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
 }
 
@@ -49,21 +49,19 @@ tasks.withType(JavaCompile) {
 	options.encoding = SOURCE_ENCODING
 }
 
-def readCurrentGitCommit() {
-	def proc = ["git", "rev-parse", "HEAD"].execute(null, project.projectDir)
-	def exitCode = proc.waitFor()
-	if (exitCode != 0) {
-		throw new IllegalStateException("git rev-parse command exited with status code ${exitCode}:\n" + proc.err.readLines().join("\n"))
-	}
-	return proc.in.readLines()[0]
+final firstLineOfProcessOutput = {ExecOutput execOutput ->
+	return execOutput.standardOutput.asText.map {it.split('\n')[0]}
 }
 
-final currentGitCommit = readCurrentGitCommit()
 processResources {
-	inputs.property("project.version", project.version)
-	inputs.property("currentGitCommit", currentGitCommit)
+	inputs.property("version", project.version)
+	inputs.property("currentGitCommit", firstLineOfProcessOutput(providers.exec {
+		executable = "git"
+		args = ["rev-parse", "HEAD"]
+	}))
+
 	filesMatching("de/prob2/jupyter/build.properties") {
-		expand(version: project.version, commit: readCurrentGitCommit())
+		expand(version: inputs.properties["version"], commit: inputs.properties["currentGitCommit"])
 	}
 }
 

gradle/wrapper/gradle-wrapper.properties

 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.6-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.13-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME

gradlew

@@ -15,6 +15,8 @@
 # See the License for the specific language governing permissions and
 # limitations under the License.
 #
+# SPDX-License-Identifier: Apache-2.0
+#
 
 ##############################################################################
 #
@@ -55,7 +57,7 @@
 #       Darwin, MinGW, and NonStop.
 #
 #   (3) This script is generated from the Groovy template
-#       https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt
+#       https://github.com/gradle/gradle/blob/HEAD/platforms/jvm/plugins-application/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt
 #       within the Gradle project.
 #
 #       You can find Gradle at https://github.com/gradle/gradle/.
@@ -84,7 +86,7 @@ done
 # shellcheck disable=SC2034
 APP_BASE_NAME=${0##*/}
 # Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036)
-APP_HOME=$( cd "${APP_HOME:-./}" > /dev/null && pwd -P ) || exit
+APP_HOME=$( cd -P "${APP_HOME:-./}" > /dev/null && printf '%s\n' "$PWD" ) || exit
 
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
@@ -203,7 +205,7 @@ fi
 DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
 
 # Collect all arguments for the java command:
-#   * DEFAULT_JVM_OPTS, JAVA_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments,
+#   * DEFAULT_JVM_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments,
 #     and any embedded shellness will be escaped.
 #   * For example: A user cannot expect ${Hostname} to be expanded, as it is an environment variable and will be
 #     treated as '${Hostname}' itself on the command line.

gradlew.bat

@@ -13,6 +13,8 @@
 @rem See the License for the specific language governing permissions and
 @rem limitations under the License.
 @rem
+@rem SPDX-License-Identifier: Apache-2.0
+@rem
 
 @if "%DEBUG%"=="" @echo off
 @rem ##########################################################################

src/main/java/de/prob2/jupyter/CommandUtils.java

@@ -409,13 +409,18 @@ public final class CommandUtils {
 			cmdExact.addKeywordContext(CompleteIdentifierCommand.KeywordContext.ALL);
 			trace.getStateSpace().execute(cmdExact);
 			// Use LinkedHashSet to remove duplicates while maintaining order.
-			final Set<String> completions = new LinkedHashSet<>(cmdExact.getCompletions());
+			final Set<String> completions = new LinkedHashSet<>();
+			for (CompleteIdentifierCommand.Completion completion : cmdExact.getCompletions()) {
+				completions.add(completion.getCompletion());
+			}
 			
 			final CompleteIdentifierCommand cmdIgnoreCase = new CompleteIdentifierCommand(prefix);
 			cmdIgnoreCase.setIgnoreCase(true);
 			cmdIgnoreCase.addKeywordContext(CompleteIdentifierCommand.KeywordContext.ALL);
 			trace.getStateSpace().execute(cmdIgnoreCase);
-			completions.addAll(cmdIgnoreCase.getCompletions());
+			for (CompleteIdentifierCommand.Completion completion : cmdExact.getCompletions()) {
+				completions.add(completion.getCompletion());
+			}
 			
 			return new ReplacementOptions(new ArrayList<>(completions), start, end);
 		};

src/main/java/de/prob2/jupyter/commands/DotCommand.java

@@ -71,7 +71,7 @@ public final class DotCommand implements Command {
 	public @NotNull String getHelpBody() {
 		final StringBuilder sb = new StringBuilder("The following dot visualisation commands are available:\n\n");
 		final Trace trace = this.animationSelector.getCurrentTrace();
-		final GetAllDotCommands cmd = new GetAllDotCommands(trace.getCurrentState());
+		final GetAllDotCommands cmd = new GetAllDotCommands(trace);
 		trace.getStateSpace().execute(cmd);
 		for (final DynamicCommandItem item : cmd.getCommands()) {
 			sb.append("* `");
@@ -99,7 +99,7 @@ public final class DotCommand implements Command {
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final DotVisualizationCommand dotCommand;
 		try {
-			dotCommand = DotVisualizationCommand.getByName(command, trace.getCurrentState());
+			dotCommand = DotVisualizationCommand.getByName(command, trace);
 		} catch (final IllegalArgumentException e) {
 			throw new UserErrorException("No such dot command: " + command, e);
 		}
@@ -131,10 +131,10 @@ public final class DotCommand implements Command {
 		return new ParameterCompleters(ImmutableMap.of(
 			COMMAND_PARAM, (commandName, at) -> {
 				final Trace trace = this.animationSelector.getCurrentTrace();
-				final GetAllDotCommands cmd = new GetAllDotCommands(trace.getCurrentState());
+				final GetAllDotCommands cmd = new GetAllDotCommands(trace);
 				trace.getStateSpace().execute(cmd);
 				final String prefix = commandName.substring(0, at);
-				final List<String> commands = DotVisualizationCommand.getAll(trace.getCurrentState())
+				final List<String> commands = DotVisualizationCommand.getAll(trace)
 					.stream()
 					.filter(DynamicCommandItem::isAvailable)
 					.map(DynamicCommandItem::getCommand)

src/main/java/de/prob2/jupyter/commands/TableCommand.java

@@ -72,7 +72,7 @@ public final class TableCommand implements Command {
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final IEvalElement formula = kernel.parseFormula(args.get(EXPRESSION_PARAM), FormulaExpand.EXPAND);
 		
-		final TableData table = TableVisualizationCommand.getByName(TableVisualizationCommand.EXPRESSION_AS_TABLE_NAME, trace.getCurrentState())
+		final TableData table = TableVisualizationCommand.getByName(TableVisualizationCommand.EXPRESSION_AS_TABLE_NAME, trace)
 			.visualize(Collections.singletonList(formula));
 		
 		final StringBuilder sbPlain = new StringBuilder();