POG PO source

[leouk]

When calling the POG, it would be useful to get location information associated with each of the POs.

[nickbattle]

The internal ProofObligations do have location information and this should navigate (double-click) from the PO list view to the location of the PO in the source, though it is awkward because a single click will expand or collapse the PO.

What's the use case here?

[leouk]

Going back to the place where the PO was generated from - which in large specs is useful, given the PO's structure is not quite "obvious". It does work (double clicking, after expanding) on 1.3.2. :-)

[nickbattle]

When we review the POG for QC, we can try to make this easier - perhaps an explicit icon to "goto source" rather than the confusing double-click that we have.