Display of Ltac debugging mode

[coquser]

Recently I often work on Ltac coding in emacs with "Set Ltac Debug." and found that it is harder to keep tracking on the changes in the context and goal made by the steps of the debugger.

In the current version of ProofGeneral those inputs (i.e. debuggers commands including return-key) and the outputs (i.e. the current goal and the next command to be executed) are shown in a single window sequentially and alternatively, which makes those outputs hard to discern.

I hope those inputs and outputs would be displayed in separate windows, just like the three-windows in non-debugging mode, in a future version of ProofGeneral.