span start vs. command start

[Makarius]

GNU Emacs 22.1.1, Ubuntu 8.04 LTS, Isabelle2009.

The span passed to isar-positions-of includes the whitespace before the actual command keyword. The latter is the start of the actual string passed on to the prover. Thus the line position comes out incorrect. For example:

theory Scratch imports Pure begin
ML {* Binding.pos_of @{binding x} *}

This produces a position with line 1, column 58, but the line should be 2. Column is garbled, too.

(Interestingly, after asserting the command the cursor jumps back to the span start. Should this be the end instead?)

[David Aspinall]

Thanks for report. Fixed now but see #278.

[David Aspinall]

Comment from Makarius:

It seems to work, although the behavior of the columns field is a bit odd. In certain situations there is no column at all (if the point is at start of line?).

Also note that columns (and offsets) need to be counted in terms of Isabelle symbols, not bytes/chars. E.g. \<forall> advances 1 position, not 9.

On the other hand, columns are never printed in human-readable format anyway. This extra detail would require a modification of the ProofGeneral print mode on the Isabelle side, and Proof General would have to be able to consume whatever markup produced here.

So I recommend to remove any attempt at column position.

[David Aspinall]

Reply from da:

OK, have removed column position for time being. Not sure why columns weren't passed at start of line.