Skip to content

Commit

Permalink
Don't trim list separators (#4596)
Browse files Browse the repository at this point in the history
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 <[email protected]>
  • Loading branch information
Scott-Guest and rv-jenkins authored Aug 22, 2024
1 parent 6aae149 commit 0055fe7
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions k-frontend/src/main/java/org/kframework/kil/UserList.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down Expand Up @@ -58,7 +58,7 @@ public String getSeparator() {
}

public void setSeparator(String separator) {
this.separator = separator.trim();
this.separator = separator;
}

@Override
Expand Down

0 comments on commit 0055fe7

Please sign in to comment.