PGIP and PGML

Each XML element in PGIP is represented by its own class. Elements which need to be extracted from PGIP messages (ie components of messages that are received from Isabelle) take pointers to libxml2 data structures, so that they can easily be composed by traversing a general XML tree built by libxml2. The method of building a PGIP parse tree from a generic XML tree is a depth-first traversal of the XML tree:

• Call the constructor for the base PGIP class, pgip_pgip with a pointer to the root node of the XML tree.
• When the constructor for one of the pgip_* classes is called, extract the relevant XML attributes from the node. For each child node in the XML tree, determine what PGIP entity it corresponds to, then call the constructor for that class, and create a link from the current class to the child.

For the PGIP messages that are sent from the mediator to Isabelle, a constructor that takes copies of the attributes and pointers to child PGIP entities is provided. Thus the PGIP tree is built from the leaf nodes up. This ensures that the message is a valid PGIP document.

Once the PGIP tree is built, it is traversed to produce the flat character array representation that can be sent to Isabelle. An example Mediator member function that does this is shown in figure 4.6. It is worth noticing that the code in this figure relies not only upon PGIP, but also upon knowledge of Isabelle's syntax.

language=C++

Figure 4.3: Building a PGIP message

The arrangement of PGML classes is similar to that of PGIP. Since PGML is only expected to be received from Isabelle and never send in the other direction, only one constructor for each of the pgml_* classes is needed.