Re: [isabelle] Line numbers vs. icons
On 12/2/2013 7:18 AM, Makarius wrote:
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and