1 (* translate formulae from Isabelle-string format to xml-format.
3 author: Walther Neuper 030701
6 use"xmlsrc/mathml.sml";
10 (*.decode Isabelle-strings to the format as seen by the user (1)
11 EXCEPT xml-coding issues (2).
12 (2) have a _reverse_ method
13 'isac.util.parser.FormalizationDigest.decodeEntities'
14 called within Formula#toSMLString in java
16 ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;
17 ad(2) decode "<" ---> "<", decode ">" ---> ">"
18 decode "&" ---> "&"
19 called for term2xml; + see "fun encode" in Frontend/interface.sml.*)
20 fun decode (str:cterm') =
22 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
23 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
24 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
25 | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
26 | dec (c::cs) = c::(dec cs)
27 in (implode o dec o explode) str:cterm' end;
30 fun strs2xml strs = foldl (op ^) ("", strs);
31 (* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
38 (*WN071016 checked that _all_ Frontend/interface.sml uses this*)
40 indt (j+i) ^ "<MATHML>\n" ^
41 indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^
42 indt (j+i) ^ "</MATHML>";
43 (*val t = str2term "equality e_";
44 writeln (term2xml 8 t);
46 <ISA> equality e_ </ISA>
49 (*version for TextIO*)
50 fun terms2xml j [] = ""
51 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
52 (*version for writeln: extra \n*)
53 fun terms2xml' j [] = ""
54 | terms2xml' j [t] = term2xml j t
55 | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;
57 (*WN060513 'cterm' means the Isabelle-type*)
59 indt (j+i) ^ "<MATHML>\n" ^
60 indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^
61 indt (j+i) ^ "</MATHML>\n";
62 (*version for TextIO*)
63 fun cterms2xml j [] = ""
64 | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;
65 (*version for writeln: extra \n*)
66 fun cterms2xml' j [] = ""
67 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;
69 (* writeln(cterms2xml 5 ["cterm1", "cterm2"]);