Key bindings for simplification/normalization of goals

[asr]

In #1851 (comment) Ulf wrote:

Right now in master:

• (no modifier): simplification
• C-u: non-normalised
• C-u C-u: normalised

I don't have strong opinions on this, but personally I use normalised more than the other two.

Andrea Vezzosi wrote here:

I would argue that we should switch the default back to fully normalised: I think it's the best default especially for users less in the know, so that they might have learnt neither the C-u C-u prefix nor what to expect from definitional equality.

I'm also agree with switching the default back to fully normalised.

[jespercockx]

Personally, I'm in favor of keeping the current behavior: normalised only helps me very rarely, since it destroys all my carefully crafted layers of abstraction. I can understand that newcomers don't find this a big problem (since they don't have as many layers of abstraction) but for me, having the default behavior be normalization would discourage me from trying to build the abstractions in the first place.

[jmchapman]

I like the current behaviour, normalized is sometimes slow and unreadable.

[WolframKahl]

On Mon, Feb 22, 2016 at 07:29:03AM -0800, James Chapman wrote:

I like the current behaviour, normalized is sometimes slow

(can be several minutes in some of my theories)

>> and unreadable.

(I've had over 120,000 lines there --- sometimes it is still
useful and essential; for quick exploration I just use the
double-click-for-matching-parentheses feature of Emacs
to skip past irrelevant material (in the case of (record { etc })
, click on the brace, not on the parenthesis),
and if I really need to analyse it, I save it into a file
and compress manually.
)

Normalised as default somehow does not feel right to me,
even though I use it most of the time.

For discoverability, perhaps the goal menu in Emacs
could include a separate entry for the normalised version?

Wolfram

[asr]

There are strong arguments for keeping the current behaviour, so I'm closing the issue.

[asr]

@WolframKahl Please edit your comment. The ellipsis on the gray box can be easily not taken into account.

[asr]

For discoverability, perhaps the goal menu in Emacs could include a separate entry for the normalised version?

I agree. Please open a new issue related to this enhancement.

[WolframKahl]

@asr I have no idea what is going on there, and why it does not even format mail quotations as it does for example in the original posting in this issue. I find nothing in the github MarkDown documentation that might explain that ellipsis: Where do I find that documented? Please feel free to fix it if you know how.

[asr]

I have no idea what is going on there, and why it does not even format mail quotations as it does for example in the original posting in this issue. I find nothing in the github MarkDown documentation that might explain that ellipsis: Where do I find that documented?

The same here.