Hi Frederic,
The "Goto PCal Source" command is documented on a help page linked to
from "The PlusCal Translator" page that is listed in the table of
contents.
I didn't mean to propose what I wrote in those two classes as stellar
examples of what documentation should be like. I just wanted to show
the level of formality that I had in mind.
Leslie