QED step has no locus assigned.

[kape1395]

I'm using the TLAPM parser to integrate it into the VSCode via the LSP server. Proof steps are annotated by the locations properly, but the QED step has no locus assigned at all. After some investigations, it looks to me that the location is lost here:

https://github.com/tlaplus/tlapm/blob/dc344b6d6e92332ba4a54f4cc86c577a9a137ecd/src/proof/p_parser.ml#L144

This line then tries to use the location. That try sounds like a workaround. It takes the location of the QED proof instead of the QED step itself.

https://github.com/tlaplus/tlapm/blob/dc344b6d6e92332ba4a54f4cc86c577a9a137ecd/src/proof/p_parser.ml#L83

I would be grateful for any pointers on how to fix it. I need that QED location to mark it as proved/failed/... in the editor.

[kape1395]

I fixed the tracking of the location for the QED step. The particular commit is linked above.

@damiendoligez, I'm not sure why doubly-wrapped values are used here, but since the step was assigned twice, I added the location information to both wrapping layers as well.

          | (QED (qed_loc, qp), ps) ->
              let loc = Loc.merge qed_loc (Util.get_locus qp) in
              let qp = Util.locate (Qed qp) loc in
              let qp = Property.assign qp Props.step sn in
              let qp = Property.assign qp qed_loc_prop qed_loc in
              let qp = Util.locate qp loc in
              let qp = Property.assign qp Props.step sn in
              let qp = Property.assign qp qed_loc_prop qed_loc in
              ([], qp, ps)

[kape1395]

Fixed in #93 .