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 info bubble.

Yes, same situation. I had made some experiments with better popups at some point, but postponed them.


	Makarius


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