From 856f768e32bd22d9fef09903ccda6e8697f950db Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 30 Nov 2018 10:41:36 +0100
Subject: [PATCH] Downgrade JetBrains annotations to 13.0 for compatibility
 with Alloy2B

ProB 2 uses Alloy2B, which uses Kotlin, which depends on version 13.0
of the JetBrains annotations. These are not fully compatible with newer
versions of the annotations (in particular, @Nullable and @NotNull do
not support TYPE_USE targets).

Because Alloy2B is distributed as an uberjar that contains all of its
dependencies, we cannot override the JetBrains annotations 13.0
dependency without excluding Alloy2B completely. So instead we have to
make our code compatible with the 13.0 annotations (which means
removing annotations in a few places).
---
 build.gradle                                     |  2 +-
 src/main/java/de/prob2/jupyter/ProBKernel.java   | 16 ++++++++--------
 .../de/prob2/jupyter/commands/CheckCommand.java  |  2 +-
 .../de/prob2/jupyter/commands/CommandUtils.java  | 10 +++++-----
 .../prob2/jupyter/commands/LoadFileCommand.java  |  2 +-
 .../de/prob2/jupyter/commands/SolveCommand.java  |  2 +-
 6 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/build.gradle b/build.gradle
index 2a23e3f..cf1920e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -40,7 +40,7 @@ configurations.all {
 dependencies {
 	compile(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.2.12-SNAPSHOT", changing: true)
 	compile(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.2.2")
-	compile(group: "org.jetbrains", name: "annotations", version: "16.0.2")
+	compile(group: "org.jetbrains", name: "annotations", version: "13.0") // Old version, required for compatibility with Kotlin (which is used by Alloy2B, which is used by ProB 2).
 	compile(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
 }
 
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index a7b3eb2..dc3999a 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -74,7 +74,7 @@ public final class ProBKernel extends BaseKernel {
 	private static final @NotNull Pattern BSYMB_COMMAND_PATTERN = Pattern.compile("\\\\([a-z]+)");
 	private static final @NotNull Pattern LATEX_FORMULA_PATTERN = Pattern.compile("(\\$\\$?)([^\\$]+)\\1");
 	
-	private static final @NotNull Map<@NotNull String, @NotNull String> BSYMB_COMMAND_DEFINITIONS;
+	private static final @NotNull Map<String, String> BSYMB_COMMAND_DEFINITIONS;
 	static {
 		final Map<String, String> map = new HashMap<>();
 		map.put("bfalse", "\\newcommand{\\bfalse}{\\mathord\\bot}");
@@ -137,8 +137,8 @@ public final class ProBKernel extends BaseKernel {
 	
 	private final @NotNull AnimationSelector animationSelector;
 	
-	private final @NotNull Map<@NotNull String, @NotNull Command> commands;
-	private final @NotNull Map<@NotNull String, @NotNull String> variables;
+	private final @NotNull Map<String, Command> commands;
+	private final @NotNull Map<String, String> variables;
 	
 	@Inject
 	private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
@@ -182,11 +182,11 @@ public final class ProBKernel extends BaseKernel {
 		this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
 	}
 	
-	public @NotNull Map<@NotNull String, @NotNull Command> getCommands() {
+	public @NotNull Map<String, Command> getCommands() {
 		return Collections.unmodifiableMap(this.commands);
 	}
 	
-	public @NotNull Map<@NotNull String, @NotNull String> getVariables() {
+	public @NotNull Map<String, String> getVariables() {
 		return this.variables;
 	}
 	
@@ -196,7 +196,7 @@ public final class ProBKernel extends BaseKernel {
 	}
 	
 	@Override
-	public @NotNull List<LanguageInfo.@NotNull Help> getHelpLinks() {
+	public @NotNull List<LanguageInfo.Help> getHelpLinks() {
 		return Collections.singletonList(new LanguageInfo.Help("ProB User Manual", "https://www3.hhu.de/stups/prob/index.php/User_Manual"));
 	}
 	
@@ -367,7 +367,7 @@ public final class ProBKernel extends BaseKernel {
 		this.animationSelector.getCurrentTrace().getStateSpace().kill();
 	}
 	
-	private @NotNull List<@NotNull String> formatErrorSource(final @NotNull List<@NotNull String> sourceLines, final @NotNull ErrorItem.Location location) {
+	private @NotNull List<String> formatErrorSource(final @NotNull List<String> sourceLines, final @NotNull ErrorItem.Location location) {
 		if (sourceLines.isEmpty()) {
 			return Collections.singletonList(this.errorStyler.primary("// Source code not known"));
 		}
@@ -414,7 +414,7 @@ public final class ProBKernel extends BaseKernel {
 	}
 	
 	@Override
-	public @NotNull List<@NotNull String> formatError(final Exception e) {
+	public @NotNull List<String> formatError(final Exception e) {
 		try {
 			LOGGER.warn("Exception while executing command from user", e);
 			if (e instanceof UserErrorException) {
diff --git a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
index e1fba4b..9251873 100644
--- a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
@@ -27,7 +27,7 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class CheckCommand implements Command {
-	private static final @NotNull Map<@NotNull String, @NotNull String> SECTION_NAME_MAP;
+	private static final @NotNull Map<String, String> SECTION_NAME_MAP;
 	static {
 		final Map<String, String> sectionNameMap = new HashMap<>();
 		sectionNameMap.put("properties", "PROPERTIES");
diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
index 1d978e1..9a9fb9e 100644
--- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
@@ -92,7 +92,7 @@ public final class CommandUtils {
 		}
 	}
 	
-	public static @NotNull List<@NotNull String> splitArgs(final @NotNull String args, final int limit) {
+	public static @NotNull List<String> splitArgs(final @NotNull String args, final int limit) {
 		final String[] split = ARG_SPLIT_PATTERN.split(args, limit);
 		if (split.length == 1 && split[0].isEmpty()) {
 			return Collections.emptyList();
@@ -101,11 +101,11 @@ public final class CommandUtils {
 		}
 	}
 	
-	public static @NotNull List<@NotNull String> splitArgs(final @NotNull String args) {
+	public static @NotNull List<String> splitArgs(final @NotNull String args) {
 		return splitArgs(args, 0);
 	}
 	
-	public static @NotNull Map<@NotNull String, @NotNull String> parsePreferences(final @NotNull List<@NotNull String> args) {
+	public static @NotNull Map<String, String> parsePreferences(final @NotNull List<String> args) {
 		final Map<String, String> preferences = new HashMap<>();
 		for (final String arg : args) {
 			final String[] split = arg.split("=", 2);
@@ -237,7 +237,7 @@ public final class CommandUtils {
 		);
 	}
 	
-	public static @Nullable DisplayData inspectArgs(final @NotNull String argString, final int at, final @NotNull Inspector @NotNull... inspectors) {
+	public static @Nullable DisplayData inspectArgs(final @NotNull String argString, final int at, final @NotNull Inspector... inspectors) {
 		final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(argString);
 		int argStart = 0;
 		int argEnd = argString.length();
@@ -256,7 +256,7 @@ public final class CommandUtils {
 		return inspectors[i].inspect(argString.substring(argStart, argEnd), at - argStart);
 	}
 	
-	public static @Nullable ReplacementOptions completeArgs(final @NotNull String argString, final int at, final @NotNull Completer @NotNull... completers) {
+	public static @Nullable ReplacementOptions completeArgs(final @NotNull String argString, final int at, final @NotNull Completer... completers) {
 		final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(argString);
 		int argStart = 0;
 		int argEnd = argString.length();
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index 6cdb234..29cc903 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -37,7 +37,7 @@ import org.slf4j.LoggerFactory;
 public final class LoadFileCommand implements Command {
 	private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(LoadFileCommand.class);
 	
-	private static final @NotNull Map<@NotNull String, @NotNull Class<? extends ModelFactory<?>>> EXTENSION_TO_FACTORY_MAP;
+	private static final @NotNull Map<String, Class<? extends ModelFactory<?>>> EXTENSION_TO_FACTORY_MAP;
 	static {
 		final Map<String, Class<? extends ModelFactory<?>>> extensionToFactoryMap = new HashMap<>();
 		extensionToFactoryMap.put("mch", ClassicalBFactory.class);
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index b12b289..729e565 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -22,7 +22,7 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class SolveCommand implements Command {
-	private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
+	private static final @NotNull Map<String, CbcSolveCommand.Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
 		.collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s));
 	
 	private final @NotNull AnimationSelector animationSelector;
-- 
GitLab