Zulip Chat Archive

Stream: lean4

Topic: Message end position


Damiano Testa (Jan 17 2023 at 17:54):

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 (Jan 17 2023 at 23:09):

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 (Jan 17 2023 at 23:42):

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 (Jan 17 2023 at 23:59):

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


Last updated: Dec 20 2023 at 11:08 UTC