From 0055fe7c67e9b2637230a518d52f0fcfd3345aad Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Wed, 21 Aug 2024 22:02:39 -0700 Subject: [PATCH] Don't trim list separators (#4596) Closes #4592 Previously, we trimmed list separators, presumably under the assumption that `#Layout` deletes all whitespace and the user may end up including redundant whitespace. This is hacky and a faulty assumption given that we allow custom `#Layout`. For now, we just remove the `trim()` call. This shouldn't cause issues downstream - I've manually checked that all `List{...}` and `NeList{...}` declarations in the EVM, C, and WASM semantics are already correct. If anything was missed, it's an easy fix. A proper solution is described in #4595 Co-authored-by: rv-jenkins --- k-frontend/src/main/java/org/kframework/kil/UserList.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/k-frontend/src/main/java/org/kframework/kil/UserList.java b/k-frontend/src/main/java/org/kframework/kil/UserList.java index 05f22b959cd..4c42c990daa 100644 --- a/k-frontend/src/main/java/org/kframework/kil/UserList.java +++ b/k-frontend/src/main/java/org/kframework/kil/UserList.java @@ -18,13 +18,13 @@ public class UserList extends ProductionItem { public UserList(Sort sort, String separator) { this.sort = sort; - this.separator = separator.trim(); + this.separator = separator; this.listType = ZERO_OR_MORE; } public UserList(Sort sort, String separator, String listType) { this.sort = sort; - this.separator = separator.trim(); + this.separator = separator; this.listType = listType; } @@ -58,7 +58,7 @@ public String getSeparator() { } public void setSeparator(String separator) { - this.separator = separator.trim(); + this.separator = separator; } @Override