Email Gateway (Aug 19 2022 at 13:07): Email Gateway (Aug 19 2022 at 13:07):From: Makarius <makarius@sketis.net>
This is how the gutter of jEdit normally works. I merely imitated the
existing ErrorList plugin here: if the gutter already shows line numbers,
icons are not drawn -- there is no space left for them.
The reasoning behind this is probably as follows: either you have a dumb
command-line tool that prints error messages with line numbers and you
navigate yourself, or you have a smart one where errors are inlined into
the source. Isabelle/jEdit follows the second model.
What was your motivation to enable line numbers in the first place?
Makarius
Email Gateway (Aug 19 2022 at 13:09):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Isabelle/jEdit, a multi-OS application, eliminates some of the
opportunity for engaging in Mac vs. PC type hostilities, but Eclipse vs.
jEdit is there to take up the slack (where I'd rather have the
continuous proving and graphical symbols of Isabelle/jEdit any day).
With Eclipse, one can have both information icons in the gutter and line
numbers, so it can be done, at least in Eclipse.
In general, I just like the extra information of line numbers, but I
need them specifically with THY files because I use another editor to
run macros that do some processing to build LaTeX files from the THY files.
I compile small sections of a THY into a PDF. My macro takes a begin and
end line number.
Regards,
GB
Email Gateway (Aug 19 2022 at 13:09):From: Makarius <makarius@sketis.net>
I have no problems to paint icons along-side the line numbers, if jEdit
provides free pixels for that.
You can try to convince the guys at http://sourceforge.net/projects/jedit/
It might actually work out, since someone has enabled line numbers by
default in recent jEdit releases, but I reverted that for Isabelle/jEdit
to get the icons back.
Makarius
Email Gateway (Aug 19 2022 at 13:10):From: Gottfried Barrow <gottfried.barrow@gmx.com>
To make a feature request, I would have to register with sourceforge,
and I try to be a part of as few Internet forums as possible. I would
make a feature request as a half-hearted demonstration to show that I do
my half-hearted part as a team player.
But, you would have to tell me that line numbers and icons can't already
coexist in the jEdit gutter, a statement I would include as part of a
feature request.
In Eclipse, it appears there are two vertical areas which make up the
gutter, an area for graphical feedback, and an area for the line numbers.
In jEdit, there are two parts, an area for display of folding, and an
area which can only (apparently) show either line numbers, or graphical
information. There is the option "Global Options / Gutter / Selection
area width (in pixels)", but when line numbers are displayed, the option
"Minimal number of digits to reserve for line numbers" takes precedence,
and only line numbers are displayed. I don't know anything about it all
other than that.
I did a few searches on the Web looking for how to show both line
numbers and icons, but I didn't find anything.
Regards,
GB
Email Gateway (Aug 19 2022 at 13:13):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I guess there's no need for that.
I though hovering over the info icon is what makes the tooltip window
show up, but it's actually hovering over the squiggly lines that does
it. Sometimes, hovering over the icon seems to do the trick, but it
could be that the mouse cursor is close enough to the squiggly line to
make it happen. Either way, the information is all the same, and
hovering over the squiggly line always works.
A man does not need info icons when squiggly lines exist.
To belabor the point, to show how it was possible to fool a tech savvy
person such as myself, if I pass my mouse cursor over a "theorem" with a
squiggly line, to get to the icon, the tooltip window will display.
If I approach the icon from the top or bottom of the gutter, with my
mouse cursor, no tooltip window is displayed. Consequently, I thought I
was getting information from the icon, when I was getting information
from the squiggly line.
The use of the Isabelle icon at the top of the PIDE window, and in the
task bar, is helpful. I use a non-modified jEdit, and the jEdit icon was
displayed for both jEdit and Isabelle/jEdit in the Windows task bar.
Thanks,
GB
Email Gateway (Aug 19 2022 at 13:13):From: Makarius <makarius@sketis.net>
Great. This proves that you have tested the latest (and last) release
candidate http://isabelle.in.tum.de/website-Isabelle2013-2-RC3 where I had
changed the application icons.
I have done myself a 1-2h tour-de-force on Windows 8, with 8 virtual
cores, and all the auto sledgehammer stuff enabled -- not a single stray
process.
A bit more than 12 hours are left before I make the final ultimate
Isabelle2013-2 snapshot ...
Makarius
Last updated: Nov 21 2024 at 12:39 UTC