One feature would be selection of the next reduction. A one-time strategy is built and reduction is done accordingly.
When moving across terms, selecting an application should highlight it, separating its two parts, idem for a lambda.
Selecting the first part of an application should highlight the chain of applications, if any.