Allow shrinking to a single symbol in fragment selector (low priority)

[david-a-wheeler]

It'd be nice to allow shrinking to a single symbol in the fragment selector, at least for symbols that aren't "parentheses-like".

• If you select -> you only get the surrounding (... -> ....), it cannot be shrunk further.
• If you select = or e. you again only get the surrounding expression; you can't shrink to 1 symbol.

Oddly, you can already get "just the symbol" when you click on "+" or "x." (infix functions). In fact, when you click on them, you by default get just the symbol, and have to expand. That behavior is okay, it just seems oddly inconsistent & I don't understand the rule it's using. (I'd love to understand why.)

I think this is low priority right now, but if paste in the fragment selection bar or pretty mode are added this ability to shrink to one symbol would become even more useful. And while neither of those are high priority for me (compared to undo/redo or full unification), they would be nice someday. So I thought I'd create this issue now :-).

[expln]

@david-a-wheeler I made changes to allow shrinking to a single symbol. This is available on dev. However, initial selection is not changed, it still will select a sequence of symbols in one case and only a single symbol in another case. The logic is as follows.

Mm-lamp tries to select what has meaning. Suppose we are clicking on the CC in |- 1 e. CC. Then only CC is selected because CC stands for the class of complex numbers, which may have meaning on its own and users may want to select only it. Mm-lamp understands this by looking at the corresponding syntax assertion. CC is placed instead of the B variable in the syntax assertion:

When clicking on e. the entire expression gets selected because e. doesn't have meaning on its own so I think users will not want to select only this symbol. So mm-lamp expands selection by one level to have something meaningful selected rightaway. Mm-lamp understands this by seeing that e. is a constant in the syntax assertion:

With the + operator, mm-lamp uses the same approach of checking the syntax assertion. But the + symbol is placed instead of the F variable, so mm-lamp "thinks" it may have a meaning on its own and selects only it:

Previously it was not possible to shrink selection to a single symbol. But with the last update it is possible now.

[expln]

This is available in version 15 https://expln.github.io/lamp/v15/index.html

[david-a-wheeler]

That's great!

While the syntax rules may not allow a single symbol, there are definitely cases where you want to copy a symbol onto another. E.g., replacing /\ with \/.