You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
currently last entered atom (must it necessarily be an atom?) is red-selected
this feels visually iffy. debatably it's good for movement context if you press left/undo, but it's not ideal for this since it will jump from selecting the whole last atom to its second-last char.
proposal: fix via cursor behavior. when there are no holes in the resultant, have the cursor move up to the whole resultant.
The text was updated successfully, but these errors were encountered:
currently last entered atom (must it necessarily be an atom?) is red-selected
this feels visually iffy. debatably it's good for movement context if you press left/undo, but it's not ideal for this since it will jump from selecting the whole last atom to its second-last char.
proposal: fix via cursor behavior. when there are no holes in the resultant, have the cursor move up to the whole resultant.
The text was updated successfully, but these errors were encountered: