add customizable variables to configure which part of a goal the goal buffer will focus on

[cipher1024]

By setting coq-prefer-top-of-conclusion to t, we get Proof General to focus on the conclusion of the first goal after displaying the list of goals of a proof. The conclusion is defined as whatever is preceded by =======. In some cases, it can be useful to mark a different part of the conclusion as the main point of interest. This PR allows the customization of that marker as well as the ability to choose where to place that marker in the window when focusing on it.

[Matafou]

Thanks. This is a good idea. I will have a look at your patch asap. Can you explain how the user does specify the part of the goal to follow? Is it by selecting some peace of it?

[cipher1024]

Here is how I use it to improve my workflow with the Iris Proof Mode (IPM). Iris encodes different kinds of assumptions in the conclusion of a goal so the conclusion you're actually interested in is not quite the same as the one you're interested in with the Iris Proof Mode.

I put these lines in my init.el file. It makes the experience with IPM nicer but non-IPM goals are also displayed nicely with these settings:

(setq coq-prefer-top-of-conclusion t) ;; this is already part of the package

(setq coq-goal-conclusion-marker ;; this will get proof general to find the last point of interest in a goal
      (rx (or "========"
              "--------------------------------------∗"
              "--------------------------------------□")))

(setq coq-center-after-focus 'middle) ;; this will get proof general to put the conclusion marker in the middle of the *goals* window. Other options are 'top and 'bottom

[cipher1024]

So the short answer to your question is: by writing a regexp that will match a piece of the goal

[cipher1024]

One more note: I made sure that the default has the same behavior as the current version.

[erikmd]

@Matafou @cipher1024 what is the status of this PR?

[Matafou]

Looks good and useful to me. Thanks again!
@cipher1024 can you add a line to the CHANGES file, rebase into one commit please?
We need to add a documentation on these variables (coq-prefer-top-of-conclusion itself isn't).

[Matafou]

For better user configuration should we merge this preference with coq-prefer-top-of-conclusion?
Currently if this one is nil then we show the end of the conclusion (of the first goal). Something like:

    (const :tag "focus on the end of the conclusion even if it hides the conclusion marker" tail)

coq-prefer-top-of-conclusioncould be left for compatibilty.
@cipher1024 what do you think?