Email Gateway (Aug 19 2022 at 08:21): Email Gateway (Aug 19 2022 at 08:21):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Email Gateway (Aug 19 2022 at 08:22):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 26 2024 at 08:19 UTC