1.1 --- a/src/Tools/isac/xmlsrc/mathml.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -13,10 +13,10 @@
1.4 'isac.util.parser.FormalizationDigest.decodeEntities'
1.5 called within Formula#toSMLString in java
1.6
1.7 - ad(1) decode "^^^" ---> "^"; see IsacKnowledge/Atools.thy;
1.8 + ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;
1.9 ad(2) decode "<" ---> "<", decode ">" ---> ">"
1.10 decode "&" ---> "&"
1.11 - called for term2xml; + see "fun encode" in FE-interface/interface.sml.*)
1.12 + called for term2xml; + see "fun encode" in Frontend/interface.sml.*)
1.13 fun decode (str:cterm') =
1.14 let fun dec [] = []
1.15 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
1.16 @@ -35,7 +35,7 @@
1.17 val indentation = 2;
1.18 val i = indentation;
1.19
1.20 -(*WN071016 checked that _all_ FE-interface/interface.sml uses this*)
1.21 +(*WN071016 checked that _all_ Frontend/interface.sml uses this*)
1.22 fun term2xml j t =
1.23 indt (j+i) ^ "<MATHML>\n" ^
1.24 indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^