[isabelle] Line numbers vs. icons
On Fri, 22 Nov 2013, Gottfried Barrow wrote:
There are also two other things which prevent me from taking full
advantage of the info you make available. In the IDE gutter, I always
have line numbers displayed. Consequently, your icons aren't displayed.
As far as I can tell, I can't show both line numbers and information
icons in the gutter.
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and