[isabelle] Reports like command/ctrl‑mouse‑hover in Output pan?
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and