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. P. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
