equal
deleted
inserted
replaced
11 EXCEPT xml-coding issues (2). |
11 EXCEPT xml-coding issues (2). |
12 (2) have a _reverse_ method |
12 (2) have a _reverse_ method |
13 'isac.util.parser.FormalizationDigest.decodeEntities' |
13 'isac.util.parser.FormalizationDigest.decodeEntities' |
14 called within Formula#toSMLString in java |
14 called within Formula#toSMLString in java |
15 |
15 |
16 ad(1) decode "^^^" ---> "^"; see IsacKnowledge/Atools.thy; |
16 ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy; |
17 ad(2) decode "<" ---> "<", decode ">" ---> ">" |
17 ad(2) decode "<" ---> "<", decode ">" ---> ">" |
18 decode "&" ---> "&" |
18 decode "&" ---> "&" |
19 called for term2xml; + see "fun encode" in FE-interface/interface.sml.*) |
19 called for term2xml; + see "fun encode" in Frontend/interface.sml.*) |
20 fun decode (str:cterm') = |
20 fun decode (str:cterm') = |
21 let fun dec [] = [] |
21 let fun dec [] = [] |
22 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs) |
22 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs) |
23 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs) |
23 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs) |
24 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs) |
24 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs) |
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; |
37 |
37 |
38 (*WN071016 checked that _all_ FE-interface/interface.sml uses this*) |
38 (*WN071016 checked that _all_ Frontend/interface.sml uses this*) |
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_"; |