2012/9/4 David Aspinall <david.aspin...@ed.ac.uk>:
> I'm guilty myself with the experiment in Trac #444 (eager window layout),
> I will revert that change (Pierre, I understand from comments it wasn't what
> you wanted anyway, do you consider #444 solved with your own fixes now?).

I did revert it by setting the enable variable to nil by default.

There was a bug when starting a script with 3 win mode pre-enabled
(resp buffer hiding the script buffer). I fixed it in coq mode with
forcing the layout-window when proof script starts:

(add-hook 'proof-activate-scripting-hook '(lambda () (when
proof-three-window-enable (proof-layout-windows))))

I am not sure this is really the right way because:

1) people may want to keep the windows layout they have settled
instead of going back to nominal layout
2) this does not solve the bug, it is only a workaround, and it is
local to coq-mode

I also changed the behavior of proof-layout: if three-windows-mode is
enabled the by default it puts resp anf goals on the right only if the
width of the frame allows it (> 180 columns by default). I think this
is what we want.

>> How about Hol light? Would you release 4.2 with the current
>> partial hol light support enabled? Or would you put hol-light
>> into comments in generic/proof-site.el?

In any case I think by default pg should not have priority on .ml
files (over tuareg or caml mode).

>> In addition to Davids list we should fix the conflict between
>> proof-electric-terminator and coq-colon-self-insert, that I
>> reported yesterday on this list.

I am on it.

ProofGeneral-devel mailing list

Reply via email to