src/Tools/isac/xmlsrc/mathml.sml
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37906 e2b23ba9df13
child 38015 67ba02dffacc
     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 "<" ---> "&lt;", decode ">" ---> "&gt;"
    1.10           decode "&" ---> "&amp;"
    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" ^