"Extend selection" doesn't properly work in equational reasoning

[marat-rkh]

Consider the following code:

\func +-swap (m n p : Nat) : m + (n + p) = n + (m + p) =>
  m + (n + p) ==< (inv $ +-assoc m n p) >==
  (m + n) + p ==< rewrite {1} (+-comm m n) idp >==
  (n + m) + p ==< +-assoc n m p >==
  n + (m + p) `qed

1. Put a caret at any position in any expression on the left side of ==<.
2. Invoke "Edit | Extend Selection" multiple times to select the whole left side (say m + (n + p) at the beginning).

Expected result: selection extends to cover the left side. Actual result: everything after => is selected.

[ice1000]

This is because how expressions are parsed. They are BinOpSequence in the Psi syntax.

You can select expressions by abusing the 'show type' action -- put your caret on ==< and invoke 'show type'. It selects the expression for you.

[ice1000]

Btw, are you a new Arend developer? You seem to be too active as a user :thinking:

[marat-rkh]

Yes, I am, on a part- time basis)

This is because how expressions are parsed. They are BinOpSequence in the Psi syntax.

But as far as I understand, it should be possible using Concrete AST.

You can select expressions by abusing the 'show type' action -- put your caret on ==< and invoke 'show type'. It selects the expression for you.

Nice, thanks for the trick)

[valis]

Now, it extends a little bit, but then jumps to the whole expression anyway.

[sxhya]

Can't reproduce