Hi Hendrik,
I am missing the documentation comment for
pg-finish-tracing-display. What is it used for?
I've just added it:
"Handle the end of possibly voluminous tracing-style output.
If the output update was slowed down, show it now"
Tracing output is defined with a regexp, it isn't used by Coq. In
Isabelle it's used when people want to debug looping simplifier rules,
etc. Special treatment is because there can be masses of output which
we don't want to eagerly parse, convert to symbols, display, etc as it's
too expensive.
(As you may have noticed I am implementing parallel background
compilation for Coq. It is working already if there is no error
in the compilation itself. I am now trying to keep the queue
region alive when proof-action-list get empty while a whole bunch
of items are waiting at a different place until the background
compilation finishes. During this I came across the call to
pg-finish-tracing-display close to the end of
proof-shell-exec-loop...)
Sounds exciting and ambitious! Let me know if I can help further.
- D.
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
