Email Gateway (Aug 19 2022 at 09:31): Email Gateway (Aug 19 2022 at 09:31):From: Holger Blasum <hbl@sysgo.com>
Dear all,
I would ask that when you ctrl+hover on a function definition
(such as mysucc in attached hover.thy) then not only the
typing information of mysucc ("nat => nat") shows up but
also the body of the function ("mysucc n = n + 1"). Or does that
feature already exist?
best,
hover.thy
Email Gateway (Aug 19 2022 at 09:31):From: John Wickerson <jpw48@cam.ac.uk>
Hi Holger,
I find that if you ctrl+click on a function name, then the focus jumps to the definition of that function.
John
Email Gateway (Aug 19 2022 at 09:31):From: Holger Blasum <hbl@sysgo.com>
Hi John,
Ctrl+Click is certainly useful and well-intentioned. But I feel jumping
with the focus disrupts workflow more than it would just show up as
tool tip (by Ctrl+hover). Also, if I understand correctly (again, maybe I
miss sth) when I use Ctrl+Click on a function name then there is no
single-key way back (like pressing "Esc" or something ...) to where
the focus was before.
Best,
Email Gateway (Aug 19 2022 at 09:31):From: Lars Noschinski <noschinl@in.tum.de>
You could try playing around with the Navigator extension.
Email Gateway (Aug 19 2022 at 09:31):From: Fabian Immler <immler@in.tum.de>
There is also jEdits command "Go to recent buffer" with its predefined
shortcut Ctrl-`.
Email Gateway (Aug 19 2022 at 09:31):From: Lawrence Paulson <lp15@cam.ac.uk>
Try using Markers.
I just wish that they worked between files, and not just within a single file.
Larry
Email Gateway (Aug 19 2022 at 09:31):From: Fabian Immler <immler@in.tum.de>
... if the definition is in a separate file.
Email Gateway (Aug 19 2022 at 09:32):From: Makarius <makarius@sketis.net>
On Mon, 17 Dec 2012, Fabian Immler wrote:
There is also jEdits command "Go to recent buffer" with its predefined
shortcut Ctrl-`.
I did not know this one yet -- Fabian is lucky with his US keyboard
layout.
Myself I do it in a more basic way: C-W to close the target buffer. This
works under the assumption that it is from the "library", i.e. you don't
care having it open or not.
2012/12/17 Lars Noschinski <noschinl@in.tum.de>:
You could try playing around with the Navigator extension.
I've found it unconvincing when I tried some months ago -- one of the
weaker jEdit plugins. It looks like really good navigation needs to be
provided as Isabelle/jEdit functionality. Don't hold your breath for the
coming release, though. If someone can point to a good specification how
this should work, lets say in Firefox, it can be accelerated. Or someone
else might sit down himself and improve the jEdit Navigator plugin
upstream.
Another idea in the pipeline is to improve the content and flexibility of
the Isabelle/jEdit popup window: it could show you the part of the
relevant source outright, or some documentation. The next release will
already have a popup that is recursively again a jEdit text area at a
small scale, but without the extra functionality sketched here.
Makarius
Email Gateway (Aug 19 2022 at 09:32):From: Holger Blasum <hbl@sysgo.com>
Hi Makarius,
On 12-17, Makarius wrote:
Another idea in the pipeline is to improve the content and
flexibility of the Isabelle/jEdit popup window: it could show you
the part of the relevant source outright, or some documentation.
That was I what I had asked for. To understand it: is the definition
of a function (or an abbreviation, another use case, this is the one
I was originally asked when showing a theory with abbreviations to
a coworker, where typing information "bool" wasn't really informative)
less "available" at run-time than its typing information?
The next release will already have a popup that is recursively again
a jEdit text area at a small scale, but without the extra
functionality sketched here.
I've noticed this - being positively surprised how smoothly the stuff just
randomly plucked from the repository today compiles and works :-)
Only that I haven't figured out yet how to enter the window without
it disappearing from (a possibly non-standard-configured) fvwm, but
it works in xfce4. But anyway, the tool tip's presentation is orthogonal
to its content (and I think the former is more important).
Best,
Email Gateway (Aug 19 2022 at 09:32):From: Makarius <makarius@sketis.net>
On Mon, 17 Dec 2012, Holger Blasum wrote:
On 12-17, Makarius wrote:
Another idea in the pipeline is to improve the content and flexibility
of the Isabelle/jEdit popup window: it could show you the part of the
relevant source outright, or some documentation.That was I what I had asked for. To understand it: is the definition of
a function (or an abbreviation, another use case, this is the one I was
originally asked when showing a theory with abbreviations to a coworker,
where typing information "bool" wasn't really informative) less
"available" at run-time than its typing information?
First one needs to think about the canonical "definition" you want to see,
which is not necessarily the actual logical definition. I did not engage
it that seriously so far, simply because it was too far off.
There is also the question about volume of formal document content emitted
by the prover towards the front-end. Types (and sorts in the coming
release) still work, but flooding with all possible term expansions by
default will pose problems. It might have to be done more lazily, or on
explicit request, but this is still underdeveloped.
The sources where you define things in a certain external form are better
suited. No additional volume produced by the prover -- they are already
there -- and no question how to present them -- you did it already
yourself.
The next release will already have a popup that is recursively again
a jEdit text area at a small scale, but without the extra
functionality sketched here.I've noticed this - being positively surprised how smoothly the stuff
just randomly plucked from the repository today compiles and works :-)
Works usually means "works for me" in a restricted sense. There are still
many issues pending for the coming release, and we are already in the
consolidation phase. To continue the "use of latest repository game"
seriously, you have to subscribe to the isabelle-dev mailing list, for
two-way information exchange: you need to know about recent moves, and we
need to get feedback about open problems. The repository is no magic door
to get the latest features earlier than others, it rather means you have
time to spend to work out issues you encounter.
Only that I haven't figured out yet how to enter the window without it
disappearing from (a possibly non-standard-configured) fvwm, but it
works in xfce4. But anyway, the tool tip's presentation is orthogonal to
its content (and I think the former is more important).
It's not quite orthogonal. Having my own window popping up, allows to
define its content. I started experimenting with that already in 2010,
and then stopped after desparation with different Java look-and-feels,
platforms, window managers. In the version for the coming release, I
actually did try twm with spontaneous focus change and it worked. You
surely have your own strange fvwm configuration. Wasn't that fvwm2 back
then in 1995? Or do you have fvwm95 with the Windows 95 retro look?
Makarius
Email Gateway (Aug 19 2022 at 09:32):From: Holger Blasum <hbl@sysgo.com>
Hi Makarius,
On 12-17, Makarius wrote:
First one needs to think about the canonical "definition" you want
to see, which is not necessarily the actual logical definition. I
did not engage it that seriously so far, simply because it was too
far off.There is also the question about volume of formal document content
emitted by the prover towards the front-end. Types (and sorts in
the coming release) still work, but flooding with all possible term
expansions by default will pose problems. It might have to be done
more lazily, or on explicit request, but this is still
underdeveloped.The sources where you define things in a certain external form are
better suited. No additional volume produced by the prover -- they
are already there -- and no question how to present them -- you did
it already yourself.
You're right what is interesting is the definition as defined by
the user, not the one internally seen by Isabelle (iirc debuggers
also do it this way). Does Isabelle internally only keep track of
where the definition begins (theory file, offset within the theory
file) or also where it ends? (The latter would allow cutting the text ...)
Works usually means "works for me" in a restricted sense. There are
still many issues pending for the coming release, and we are already
in the consolidation phase. To continue the "use of latest
repository game" seriously, you have to subscribe to the
isabelle-dev mailing list, for two-way information exchange: you
need to know about recent moves, and we need to get feedback about
open problems. The repository is no magic door to get the latest
features earlier than others, it rather means you have time to spend
to work out issues you encounter.
Understood. In this case I was simply once-only checking whether
the feature I was looking for perhaps was already implemented in
head, and for that I was happy to get the thing started at all ...
Cannot claim serious commitment to bleeding edge per se.
You surely have your own strange fvwm configuration.
Wasn't that fvwm2 back then in 1995? Or do you have fvwm95 with the
Windows 95 retro look?
Checked this (should have done so before), it was really just my
configuration, e.g. works fine with fvwm default configuration when
wheezy debian package is just installed without fiddling. Further
inspection revealed that inserting "Style jEdit* SloppyFocus" also fixes
the disappearing jEdit subwindow for my configuration (without having to use
SloppyFocus elsewhere). I also begin to see the usefulness of
the new-window feature because it allows (combined with above request for
putting meaningful text into it) that definitions or abbreviations could
be unfolded step-by-step to arbitrary depth by the user.
best,
Email Gateway (Aug 19 2022 at 09:35):From: Makarius <makarius@sketis.net>
On Tue, 18 Dec 2012, Holger Blasum wrote:
You're right what is interesting is the definition as defined by the
user, not the one internally seen by Isabelle (iirc debuggers also do it
this way). Does Isabelle internally only keep track of where the
definition begins (theory file, offset within the theory file) or also
where it ends? (The latter would allow cutting the text ...)
There is sufficient information to determine the full definition range,
lets say the language element like "fun ..." with all its equations, or
"function ..." with the following proof. For the latter example there is
a special case, though: there is a second part following somewhere as
"termination ..." which is not directly connected.
Anything else should work smoothly, one the reference to sources is wired
up properly in the editor.
Further inspection revealed that inserting "Style jEdit* SloppyFocus"
also fixes the disappearing jEdit subwindow for my configuration
(without having to use SloppyFocus elsewhere).
I will look at this again myself. Someone else has reported focus
inversion problems with the latest Unity/Compiz of Ubuntu 12.10, so this
might be more than just an incident of vintage window managers.
Makarius
Email Gateway (Aug 19 2022 at 09:36):From: Lars Noschinski <noschinl@in.tum.de>
No. At the moment, this information is unfortunately not available (as
these theories are part of the heap image and were not processed in your
jEdit session. To my knowledge, making this information available is on
Makarius' list of things to do, but there are a lot of things on this
list ;)
-- Lars
Email Gateway (Aug 19 2022 at 09:47):From: Holger Blasum <hbl@sysgo.com>
Hello Makarius,
On 12-22, Makarius wrote:
On Tue, 18 Dec 2012, Holger Blasum wrote:
You're right what is interesting is the definition as defined by
the user, not the one internally seen by Isabelle (iirc debuggers
also do it this way). Does Isabelle internally only keep track of
where the definition begins (theory file, offset within the theory
file) or also where it ends? (The latter would allow cutting the
text ...)There is sufficient information to determine the full definition
range, lets say the language element like "fun ..." with all its
equations, or "function ..." with the following proof. For the
latter example there is a special case, though: there is a second
part following somewhere as "termination ..." which is not directly
connected.Anything else should work smoothly, one the reference to sources is
wired up properly in the editor.
"Sufficient information to determine the full definition range"
sounds promising :-)
Why am I asking whether the end point information is available?
To my post of 17 Dec I attached a file hover.thy:
If we know that the definition of "mysucc" is in file hover.thy,
characters 0x49 to 0x5a, then it could perhaps be easy to implement
to display this information (that is, in this example, "mysucc n = n + 1")
once you ctrl+hover on mysucc (without having to jump through
the theories). From a usage perspective, I think
this could be very convenient, especially if one reads a theory
sb else has written ("what was this abbreviation she is using ...").
Further inspection revealed that inserting "Style jEdit*
SloppyFocus" also fixes the disappearing jEdit subwindow for my
configuration (without having to use SloppyFocus elsewhere).I will look at this again myself. Someone else has reported focus
inversion problems with the latest Unity/Compiz of Ubuntu 12.10, so
this might be more than just an incident of vintage window managers.
Thanks for properly fixing this. That is, fvwm-wise, it now works not
only with fvwm SloppyFocus pointer focus model, but also with the fvwm
FocusFollowsMouse pointer focus model.
Happy 2013,
Email Gateway (Aug 19 2022 at 09:58):From: Makarius <makarius@sketis.net>
The "definition range" is the whole command span, starting with
"definition ..." and ending with "mysucc n = n + 1" in this example.
This is what I meant to show in the popup eventually.
In general, there is not just one equation defining a term, e.g. in "fun"
with several recursive equations, or several functions defined at the same
time. Showing the whole specification text should give sufficient clues
to the user. Lets see again how it looks when it is actually there (not
in the coming release.)
Makarius
Email Gateway (Aug 19 2022 at 09:59):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
I have a simple question (request?) considering this topic of discussion.
I find this
feature extremely helpful, especially when after Ctrl+Hover+click
transfers me
a definition/rule/lemma in any theory which happens to be part of Main.
For instance, in the last few days I have been a bit engaged in writing
detailed
proofs in Isar which are concerned with the splitting of if´s. So after
jumping
to HOL.thy and examining the split_if lemma I wanted to continue
using this (Ctrl+Hover+Click) feature and jumping to the definition of the
case_split rule, for
example.
But this feature does not seem to available any more in the file HOL.thy or
any other
theory loaded in jedit and which is part of Main. Am I doing
something wrong here [...probably...]?
Best!
Last updated: Apr 30 2024 at 12:28 UTC