476 XML.Elem (("THEOREM", []), [ |
476 XML.Elem (("THEOREM", []), [ |
477 XML.Elem (("ID", []), [XML.Text ID]), |
477 XML.Elem (("ID", []), [XML.Text ID]), |
478 XML.Elem (("FORMULA", []), [ |
478 XML.Elem (("FORMULA", []), [ |
479 XML.Text form])]) (* repair for MathML: use term instead String *) |
479 XML.Text form])]) (* repair for MathML: use term instead String *) |
480 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *) |
480 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *) |
481 fun xml_of_thm'' ((ID, term) : thm'') = |
481 fun xml_of_thm'' ((ID, thm) : thm'') = |
482 (*---xml_of_thm''------------------------------------------thm'_to_thm''-------------- |
482 (*---xml_of_thm''------------------------------------------thm'_to_thm''-------------- |
483 XML.Elem (("THEOREM", []), [ |
483 XML.Elem (("THEOREM", []), [ |
484 XML.Elem (("ID", []), [XML.Text ID]), |
484 XML.Elem (("ID", []), [XML.Text ID]), |
485 xml_of_term_NEW term]) |
485 xml_of_term_NEW term]) |
486 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*) |
486 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*) |
487 XML.Elem (("THEOREM", []), [ |
487 XML.Elem (("THEOREM", []), [ |
488 XML.Elem (("ID", []), [XML.Text ID]), |
488 XML.Elem (("ID", []), [XML.Text ID]), |
489 XML.Elem (("FORMULA", []), [ |
489 XML.Elem (("FORMULA", []), [ |
490 XML.Text (term2str term)])]) (* repair for MathML: use term instead String *) |
490 XML.Text ((term2str o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *) |
491 |
491 |
492 fun xml_to_thm' |
492 fun xml_to_thm' |
493 (XML.Elem (("THEOREM", []), [ |
493 (XML.Elem (("THEOREM", []), [ |
494 XML.Elem (("ID", []), [XML.Text ID]), |
494 XML.Elem (("ID", []), [XML.Text ID]), |
495 XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) = |
495 XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) = |
504 (ID, xml_to_term_NEW xterm) : thm'' |
504 (ID, xml_to_term_NEW xterm) : thm'' |
505 | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x) |
505 | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x) |
506 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*) |
506 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*) |
507 (XML.Elem (("THEOREM", []), [ |
507 (XML.Elem (("THEOREM", []), [ |
508 XML.Elem (("ID", []), [XML.Text ID]), |
508 XML.Elem (("ID", []), [XML.Text ID]), |
509 XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *) |
509 XML.Elem (("FORMULA", []), [ |
510 XML.Text term])])) = ((ID, str2term term) : thm'') |
510 XML.Text term])])) = (ID, assoc_thm'' (Isac ()) ID) : thm'' |
511 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x) |
511 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x) |
512 |
512 |
513 fun xml_of_src EmptyScr = |
513 fun xml_of_src EmptyScr = |
514 XML.Elem (("NOCODE", []), [XML.Text "empty"]) |
514 XML.Elem (("NOCODE", []), [XML.Text "empty"]) |
515 | xml_of_src (Prog term) = |
515 | xml_of_src (Prog term) = |