|
1 (* translate formulae from Isabelle-string format to xml-format. |
|
2 TODO implement MathML |
|
3 author: Walther Neuper 030701 |
|
4 (c) isac-team 2003 |
|
5 |
|
6 use"xmlsrc/mathml.sml"; |
|
7 use"mathml.sml"; |
|
8 *) |
|
9 |
|
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 |
|
15 |
|
16 ad(1) decode "^^^" ---> "^"; see IsacKnowledge/Atools.thy; |
|
17 ad(2) decode "<" ---> "<", decode ">" ---> ">" |
|
18 decode "&" ---> "&" |
|
19 called for term2xml; + see "fun encode" in FE-interface/interface.sml.*) |
|
20 fun decode (str:cterm') = |
|
21 let fun dec [] = [] |
|
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; |
|
28 |
|
29 |
|
30 fun strs2xml strs = foldl (op ^) ("", strs); |
|
31 (* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]); |
|
32 <XXX> xxx </XXX> |
|
33 <YYY> yyy </YYY>*) |
|
34 |
|
35 val indentation = 2; |
|
36 val i = indentation; |
|
37 |
|
38 (*WN071016 checked that _all_ FE-interface/interface.sml uses this*) |
|
39 fun term2xml j t = |
|
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); |
|
45 <MATHML> |
|
46 <ISA> equality e_ </ISA> |
|
47 <MATHML> *) |
|
48 |
|
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; |
|
56 |
|
57 (*WN060513 'cterm' means the Isabelle-type*) |
|
58 fun cterm2xml j ct = |
|
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; |
|
68 |
|
69 (* writeln(cterms2xml 5 ["cterm1", "cterm2"]); |
|
70 <MATHML> |
|
71 <ISA> cterm1 </ISA> |
|
72 </MATHML> |
|
73 <MATHML> |
|
74 <ISA> cterm2 </ISA> |
|
75 </MATHML> |
|
76 *) |