26 | dec (c::cs) = c::(dec cs) |
26 | dec (c::cs) = c::(dec cs) |
27 in (implode o dec o explode) str:cterm' end; |
27 in (implode o dec o explode) str:cterm' end; |
28 |
28 |
29 |
29 |
30 fun strs2xml strs = foldl (op ^) ("", strs); |
30 fun strs2xml strs = foldl (op ^) ("", strs); |
31 (* tracing (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]); |
31 (* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]); |
32 <XXX> xxx </XXX> |
32 <XXX> xxx </XXX> |
33 <YYY> yyy </YYY>*) |
33 <YYY> yyy </YYY>*) |
34 |
34 |
35 val indentation = 2; |
35 val indentation = 2; |
36 val i = indentation; |
36 val i = indentation; |
39 fun term2xml j t = |
39 fun term2xml j t = |
40 indt (j+i) ^ "<MATHML>\n" ^ |
40 indt (j+i) ^ "<MATHML>\n" ^ |
41 indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^ |
41 indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^ |
42 indt (j+i) ^ "</MATHML>"; |
42 indt (j+i) ^ "</MATHML>"; |
43 (*val t = str2term "equality e_"; |
43 (*val t = str2term "equality e_"; |
44 tracing (term2xml 8 t); |
44 writeln (term2xml 8 t); |
45 <MATHML> |
45 <MATHML> |
46 <ISA> equality e_ </ISA> |
46 <ISA> equality e_ </ISA> |
47 <MATHML> *) |
47 <MATHML> *) |
48 |
48 |
49 (*version for TextIO*) |
49 (*version for TextIO*) |
50 fun terms2xml j [] = "" |
50 fun terms2xml j [] = "" |
51 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts; |
51 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts; |
52 (*version for tracing: extra \n*) |
52 (*version for writeln: extra \n*) |
53 fun terms2xml' j [] = "" |
53 fun terms2xml' j [] = "" |
54 | terms2xml' j [t] = term2xml j t |
54 | terms2xml' j [t] = term2xml j t |
55 | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts; |
55 | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts; |
56 |
56 |
57 (*WN060513 'cterm' means the Isabelle-type*) |
57 (*WN060513 'cterm' means the Isabelle-type*) |
60 indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^ |
60 indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^ |
61 indt (j+i) ^ "</MATHML>\n"; |
61 indt (j+i) ^ "</MATHML>\n"; |
62 (*version for TextIO*) |
62 (*version for TextIO*) |
63 fun cterms2xml j [] = "" |
63 fun cterms2xml j [] = "" |
64 | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts; |
64 | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts; |
65 (*version for tracing: extra \n*) |
65 (*version for writeln: extra \n*) |
66 fun cterms2xml' j [] = "" |
66 fun cterms2xml' j [] = "" |
67 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts; |
67 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts; |
68 |
68 |
69 (* tracing(cterms2xml 5 ["cterm1", "cterm2"]); |
69 (* writeln(cterms2xml 5 ["cterm1", "cterm2"]); |
70 <MATHML> |
70 <MATHML> |
71 <ISA> cterm1 </ISA> |
71 <ISA> cterm1 </ISA> |
72 </MATHML> |
72 </MATHML> |
73 <MATHML> |
73 <MATHML> |
74 <ISA> cterm2 </ISA> |
74 <ISA> cterm2 </ISA> |