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 MHonArc.