Merge lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913 into lp:tapaal
Proposed by
Lena Ernstsen
Status: | Merged | ||||
---|---|---|---|---|---|
Approved by: | Jiri Srba | ||||
Approved revision: | 1124 | ||||
Merged at revision: | 1126 | ||||
Proposed branch: | lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913 | ||||
Merge into: | lp:tapaal | ||||
Diff against target: |
38 lines (+15/-4) 2 files modified
src/pipe/gui/Pipe.java (+1/-1) src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+14/-3) |
||||
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/token-truncation-bug-1918913 | ||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+400594@code.launchpad.net |
This proposal supersedes a proposal from 2021-03-27.
Commit message
Every digit of the token count is now visible
Description of the change
Made it possible to see more than the 3 most significant digits for the token counts.
However, maximum number of digits is 8, as an "out of memory" error appears with 9 or more digits.
To post a comment you must log in.
It looks as an okay solution. Can the limit of 999 tokens when drawing the net in GUI be increased to say 99999999 tokens? Should some net exceed it when loading, then print >9999 9999 instead of #9999 9999 (just to be sure).