263 fun xml_of_asm_val (asm, vl) = |
263 fun xml_of_asm_val (asm, vl) = |
264 XML.Elem (("ASMEVALUATED", []),[ |
264 XML.Elem (("ASMEVALUATED", []),[ |
265 XML.Elem (("ASM", []), [xml_of_term asm]), |
265 XML.Elem (("ASM", []), [xml_of_term asm]), |
266 XML.Elem (("VALUE", []), [xml_of_term vl])]) |
266 XML.Elem (("VALUE", []), [xml_of_term vl])]) |
267 |
267 |
268 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, where_) = |
268 fun xml_of_matchpbl (model_ok, _(*pI*), hdl, pbl, where_) = |
269 XML.Elem (("CONTEXTDATA", []), [ |
269 XML.Elem (("CONTEXTDATA", []), [ |
270 XML.Elem (("GUH", []), [(XML.Text "would-need-ctxt")(*XML.Text (Ptool.pblID2guh pI)*)]), |
270 XML.Elem (("GUH", []), [(XML.Text "would-need-ctxt")(*XML.Text (Ptool.pblID2guh pI)*)]), |
271 XML.Elem (("STATUS", []), [ |
271 XML.Elem (("STATUS", []), [ |
272 XML.Text ((if model_ok then "correct" else "incorrect"))]), |
272 XML.Text ((if model_ok then "correct" else "incorrect"))]), |
273 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]), |
273 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]), |