Description of the printy(tup) SETL procedure

This procedure organizes printing and output into two "phases". During the first phase, printing of proofs is direct; during the second phase, messages received are separated into a report stream and a error stream, and formatted into html tables.

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

182Theorem 116 14F (m,n - m) --> T189 ==> #(m + (n - m)) = m ĄPLUS (n - m)
Explanatory remark
The .php server code associated with error display prefixes these generated lines with header lines having the form
EtnaNova Preliminary - Verification Failures Report
"
Thm. No.Thm. Name Line No.F/ALine
and then echoes all the preceding lines to the client, followed by a concluding block of the form