fix: whitespace after the box operator, causing [][Next] to be reformatted to [] [Next]

PrefixExprConstruct.java used z[0].getImage().length() > 1 to decide spacing, but getImage() returns SANY's internal node name (N_GenPrefixOp) — always long — so it always added a space.

Changed to Character.isLetter(z[0].getHumanReadableImage().charAt(0)) — uses the actual operator text ([], DOMAIN, etc.) and checks if it starts with a letter (keyword → space, symbol → no space)

Author: Copilot

src/main/java/me/fponzi/tlaplusformatter/constructs/impl/PrefixExprConstruct.java

@@ -27,7 +27,7 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
         var z = node.zero();
         var genInfixOp = context.buildChild(z[0]);
         var val = context.buildChild(z[1]);
-        if (z[0].getImage().length() > 1) {
+        if (Character.isLetter(z[0].getHumanReadableImage().charAt(0))) {
             // e.g., DOMAIN, SUBSET etc.
             return genInfixOp.appendSpace(val);
         }

src/test/java/me/fponzi/tlaplusformatter/constructs/impl/PrefixExprConstructTest.java

@@ -0,0 +1,58 @@
+package me.fponzi.tlaplusformatter.constructs.impl;
+
+import org.junit.jupiter.api.Test;
+
+import static me.fponzi.tlaplusformatter.Utils.assertUnchanged;
+
+public class PrefixExprConstructTest {
+
+    @Test
+    void testBoxOperatorNoSpaceWithActionExpr() {
+        var s = "----- MODULE Test -----\n" +
+                "VARIABLE x\n" +
+                "Next == x' = x\n" +
+                "Spec == [][Next]_x\n" +
+                "====";
+        assertUnchanged(s);
+    }
+
+    @Test
+    void testBoxOperatorNoSpaceWithIdentifier() {
+        var s = "----- MODULE Test -----\n" +
+                "VARIABLE x\n" +
+                "Inv == x = 0\n" +
+                "Prop == []Inv\n" +
+                "====";
+        assertUnchanged(s);
+    }
+
+    @Test
+    void testDiamondOperatorNoSpace() {
+        var s = "----- MODULE Test -----\n" +
+                "VARIABLE x\n" +
+                "Inv == x = 0\n" +
+                "Prop == <>Inv\n" +
+                "====";
+        assertUnchanged(s);
+    }
+
+    @Test
+    void testDomainHasSpace() {
+        var s = "----- MODULE Test -----\n" +
+                "VARIABLE f\n" +
+                "op == DOMAIN f\n" +
+                "====";
+        assertUnchanged(s);
+    }
+
+    @Test
+    void testSubsetHasSpace() {
+        var s = "----- MODULE Test -----\n" +
+                "EXTENDS Naturals\n" +
+                "VARIABLE x\n" +
+                "op == SUBSET x\n" +
+                "====";
+        assertUnchanged(s);
+    }
+
+}

src/test/resources/outputs/AllConstructs.tla

@@ -51,7 +51,7 @@ Power(U) == SUBSET U
 BigUnion(A) == UNION A
 
 CaseExample(u) == CASE u \in Nat -> u + 1
-                  [] u \in Int \ Nat -> - u
+                  [] u \in Int \ Nat -> -u
                   [] OTHER-> 0
 
 IfElseExample(b, e1, e2) == IF b THEN e1 ELSE e2
@@ -112,7 +112,7 @@ Init == /\ x = 0
 
 IncX == x' = x + 1
 DecX == x' = x - 1
-ToggleQ == q' = ~ q
+ToggleQ == q' = ~q
 AssignY == \E n \in 0 .. N: y' = n
 UpdateZ == \E e \in S: z' = z \cup { e }
 BumpFAny == \E i \in DOMAIN f: f' = [f EXCEPT ![i] = @ + 1]
@@ -130,13 +130,13 @@ Next == \/ ( IncX /\ UNCHANGED << y, z, f, r, s, q >> )
         \/ ( AppendS /\ UNCHANGED << x, y, z, f, r, q >> )
         \/ Stutter
 
-Spec == Init /\ [] [Next]_vars /\ WF_vars(IncX) /\ SF_vars(AssignY)
+Spec == Init /\ [][Next]_vars /\ WF_vars(IncX) /\ SF_vars(AssignY)
 
-Invariance == [] TypeInv
+Invariance == []TypeInv
 LeadsToExample == ( x < N ) ~> ( x = N )
 
 EnablementExample == /\ ENABLED IncX
-                     /\ ~ ENABLED DecX
+                     /\ ~ENABLED DecX
 
 ---- MODULE SimpleImported ----
 EXTENDS Naturals, Sequences

src/test/resources/outputs/HourClock.tla

@@ -5,9 +5,9 @@ EXTENDS Naturals, TLC
 VARIABLE hr
 HCini == hr \in ( 1 .. 12 )
 HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
-HC == HCini /\ [] [HCnxt]_hr
+HC == HCini /\ [][HCnxt]_hr
 --------------------------------------------------------------
-THEOREM HC => [] HCini
+THEOREM HC => []HCini
 ==============================================================
 This is post text
 Has multiple lines in it.

src/test/resources/outputs/Slush.tla

@@ -286,7 +286,7 @@ Init ==
 
 QueryReplyLoop(self) ==
   /\ pc[self] = "QueryReplyLoop"
-  /\ IF ~ Terminate
+  /\ IF ~Terminate
      THEN /\ pc' = [pc EXCEPT ![self] = "WaitForQueryMessageOrTermination"]
      ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
   /\ UNCHANGED << pick, message, sampleSet, loopVariant >>
@@ -424,9 +424,9 @@ Next ==
       ( \E self \in SlushLoopProcess: SlushLoop(self) ) \/
     Terminating
 
-Spec == Init /\ [] [Next]_vars
+Spec == Init /\ [][Next]_vars
 
-Termination == <> ( \A self \in ProcSet: pc[self] = "Done" )
+Termination == <>( \A self \in ProcSet: pc[self] = "Done" )
 
 
 \* END TRANSLATION

src/test/resources/outputs/Stones.tla

@@ -75,7 +75,7 @@ Partitions(seq, wt) ==
 (* of the sequence seq sum to wt.                                          *)
 (***************************************************************************)
 Weighs(seq, wt) ==
-  \E coef \in [1 .. N -> - 1 .. 1]:
+  \E coef \in [1 .. N -> -1 .. 1]:
     SeqSum([i \in 1 .. N |-> coef[i] * seq[i]]) = wt
 
 (***************************************************************************)