Re: [isabelle] Reports like command/ctrl‑mouse‑hover in Output pan?
On Tue, 21 Aug 2012, Yannick Duchêne (Hibou57) wrote:
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.
It is one of obvious the things that are just missing (but more important
than imitating Proof General menus). The output box is an HTML4 component
with its own rules, not an editor buffer. I had postponed too
sophisticated functionality there, bacause I was waiting for Sun/Oracle's
HTML5 component to be shipped with JDK. This has happened just last week
with Java 7u6, and I will see soon if the time of waiting was worthwhile.
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
Yes, same situation. I had made some experiments with better popups at
some point, but postponed them.
This archive was generated by a fusion of
Pipermail (Mailman edition) and