And allow ! types for imports of inv_T

nickbattle · Dec 1, 2023 · a8d65ee · a8d65ee
1 parent 7b509ab
commit a8d65ee
Showing 1 changed file with 13 additions and 1 deletion.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java
@@ -655,7 +655,19 @@ private ASTImportedFunction readImportedFunction(LexIdentifierToken from)
 		if (lastToken().is(Token.COLON))
 		{
 			nextToken();
-			type = getTypeReader().readType();
+
+			// Allow maximal ! for inv_T functions
+			boolean saved = Properties.parser_maximal_types;
+
+			try
+			{
+				Properties.parser_maximal_types = true;
+				type = getTypeReader().readType();
+			}
+			finally
+			{
+				Properties.parser_maximal_types = saved;
+			}
 		}
 
 		LexNameToken renamed = null;