63 fun strs2xml strs = foldl (op ^) ("", strs); |
63 fun strs2xml strs = foldl (op ^) ("", strs); |
64 |
64 |
65 (*WN071016 checked that _all_ Frontend/interface.sml uses this*) |
65 (*WN071016 checked that _all_ Frontend/interface.sml uses this*) |
66 fun term2xml j t = |
66 fun term2xml j t = |
67 indt (j+i) ^ "<MATHML>\n" ^ |
67 indt (j+i) ^ "<MATHML>\n" ^ |
68 indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^ |
68 indt (j+2*i) ^ "<ISA> " ^ (decode o TermC.unparse_ERROR) t ^ " </ISA>\n" ^ |
69 indt (j+i) ^ "</MATHML>"; |
69 indt (j+i) ^ "</MATHML>"; |
70 (*val t = TermC.parse_test @{context} "equality e_"; |
70 (*val t = TermC.parse_test @{context} "equality e_"; |
71 writeln (term2xml 8 t); |
71 writeln (term2xml 8 t); |
72 <MATHML> |
72 <MATHML> |
73 <ISA> equality e_ </ISA> |
73 <ISA> equality e_ </ISA> |
74 <MATHML> *) |
74 <MATHML> *) |
75 fun xml_of_term t = |
75 fun xml_of_term t = |
76 XML.Elem (("MATHML", []), |
76 XML.Elem (("MATHML", []), |
77 [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])]) |
77 [XML.Elem (("ISA", []), [XML.Text ((decode o TermC.unparse_ERROR) t)])]) |
78 fun xml_of_terms ts = map xml_of_term ts |
78 fun xml_of_terms ts = map xml_of_term ts |
79 |
79 |
80 (* intermediate replacements while introducing transfer of terms by libisabelle *) |
80 (* intermediate replacements while introducing transfer of terms by libisabelle *) |
81 fun xml_of_term_NEW (t : term) = |
81 fun xml_of_term_NEW (t : term) = |
82 XML.Elem (("FORMULA", []), [ |
82 XML.Elem (("FORMULA", []), [ |
83 XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)]), |
83 XML.Elem (("ISA", []), [XML.Text ((decode o TermC.unparse_ERROR) t)]), |
84 XML.Text ("(TERM)\n " ^ UnparseC.term t ^ "\n(/TERM)") |
84 XML.Text ("(TERM)\n " ^ UnparseC.term t ^ "\n(/TERM)") |
85 ]) |
85 ]) |
86 |
86 |
87 (*version for TextIO*) |
87 (*version for TextIO*) |
88 fun terms2xml _ [] = "" |
88 fun terms2xml _ [] = "" |