Message end position

Stream: lean4

[Damiano Testa]

Dear All,

as far as I understand, the docs4#Lean.Message associated with the code

#eval let n := 0
      n

has a Position and an endPos, which point both to the line on which the #eval is (depending on how you count, you could say that they point to the line below the #eval).

Is there some record of the position where the command ends? If I did this correctly, these are the Positions that I find:

Message.pos: ⟨1, 0⟩
Message.endPos: some (⟨1, 5⟩)

I would like

Message.actualEnd: ⟨2, [I do not really care about the column]⟩

informing me that the #eval block spans two lines.

[James Gallicchio]

I believe message positions are orthogonal to syntax positions. So while the message here occurs at line 1, the syntax spans lines 1-2. If you have access to the syntax object you should be able to get the positions somehow (not entirely sure how)

[Damiano Testa]

Thank you very much! I think that if s : Frontend.State, then s.commands.map (Syntax.getPos? ·) s.commands.map (Syntax.getTailPos? ·) returns a list that seems to contain at least all the positions that I want!

I will have to experiment to see if I need to sift out unwanted positions, but this is very helpful, thanks!

[Damiano Testa]

Small correction: docs4#Lean.Syntax.getPos? seems to be the initial position. The end position is docs4#Lean.Syntax.getTailPos?.