During phase 2 this sorts the printed output into "success" and "error" streams, formatting them both and directing them to different files. "error" stream formatting works as follows: Lines starting with "++++++++" are suppressed, but the theorem name and line number are extracted from them and retained. Then, when a line containing '****** Error verifying step:' is encountered, we extract the step number, and (from the next two lines) the offending statement and the "remark" describing the offense. Subsequent material from the same error record is written to a secondary error file, and we keep track of the starting and encing characters of the section of this file that corresponds to each verification error. The fields describing the error line itself are assembled into an HTML table row string of the form
The .php server code associated with error display prefixes these generated lines with header lines having the form