From 6d45d1506455b9991ef56c69e1526466e841773d Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Thu, 26 Jun 2025 13:30:33 +0200
Subject: [PATCH] Fix @generated comment in machine file header
---
src/main/java/de/tla2bAst/Translator.java | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index b89c3bd..8eb569c 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -37,7 +37,12 @@ import java.util.stream.Collectors;
import static de.tla2b.global.TranslationGlobals.VERSION_NUMBER;
public class Translator {
- private static final String GENERATED_BY_TLA2B_HEADER = "/*@ generated by TLA2B ";
+
+ /**
+ * This old header looks like the generated pragma which does not parse because of the text following it.
+ */
+ private static final String GENERATED_BY_TLA2B_HEADER_OLD = "/*@ generated by TLA2B ";
+ private static final String GENERATED_BY_TLA2B_HEADER = "/* @generated by TLA2B ";
private String parentPath;
private File moduleFile;
@@ -216,7 +221,8 @@ public class Translator {
if (machineFile.exists()) {
try (BufferedReader in = new BufferedReader(new FileReader(machineFile))) {
String firstLine = in.readLine();
- if (firstLine != null && !firstLine.startsWith(GENERATED_BY_TLA2B_HEADER)) {
+ boolean generatedByTLA2B = firstLine != null && (firstLine.startsWith(GENERATED_BY_TLA2B_HEADER_OLD) || firstLine.startsWith(GENERATED_BY_TLA2B_HEADER));
+ if (!generatedByTLA2B) {
System.err.println("Error: File " + machineFile.getName() + " already exists"
+ " and was not generated by TLA2B.\n" + "Delete or move this file.");
System.exit(-1);
--
GitLab