[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?


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.