[isabelle] Reports like command/ctrl‑mouse‑hover in Output pan?

Hi all,

I wanted to know if there is a way to get in the output pan, the same kind of report as the one you have in an info‑bubble when the mouse is over an identifier while you press command or ctrl.

When there are a lot of things in the info bubble, it sometime disappears to much quickly, and also, you cannot copy/past from an the info bubble.

I had a look at all “print_*”, but could not find something.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.