debugging messages delayed in proof general

[alleystoughton]

In examples/debugging-delay on deploy-interpreter, there is an example showing how debugging message are delayed under proof general, but not when run from the shell:

If you run testing.uci from the shell, there is a pause between the debugging message saying

trying to prove truth or falsity of: adv <= (func, 1).1 \/ adv <> (adv, 2).1 \/ (adv, 2).`2 < 0

and the message

formula's negation proved

But in proof general the message come out - after the pause - at once.

[01tomislav]

I tested this on Ubuntu, the behaviour is slightly different. The debugging message

trying to prove truth or falsity of: adv <= (func, 1).`1 \/ adv <> (adv, 2).`1 \/ (adv, 2).`2 < 0

shows up on time, however the message

formula simplified to: adv <= func

is delayed. On the other hand, the uc dsl interpreter buffer seems to be on time, except failing to output the closing tag. My guess is this is where the problem is. The are marked for eager annotation. An "eager annotation indicates" to Proof General that some following output should be displayed (or processed) immediately and not accumulated for parsing later. So there should be no delay, except when the closing tag is missing.