(* translate formulae from Isabelle-string format to xml-format.

   TODO implement MathML

   author: Walther Neuper 030701

   (c) isac-team 2003

use"xmlsrc/mathml.sml";

use"mathml.sml";

*)

(*.decode Isabelle-strings to the format as seen by the user (1)

   EXCEPT xml-coding issues (2).

   (2) have a _reverse_ method 

   'isac.util.parser.FormalizationDigest.decodeEntities' 

   called within Formula#toSMLString in java

   ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;

   ad(2) decode "<" ---> "&lt;", decode ">" ---> "&gt;"

         decode "&" ---> "&"

   called for term2xml; + see "fun encode" in Frontend/interface.sml.*)

fun decode (str:cterm') = 

    let fun dec [] = []

	  | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)

	  | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)

	  | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)

	  | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)

	  | dec (c::cs) = c::(dec cs)

    in (implode o dec o explode) str:cterm' end;

fun strs2xml strs = foldl (op ^) ("", strs); 

(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);

<XXX> xxx </XXX>

<YYY> yyy </YYY>*)

val indentation = 2;

val i = indentation;

(*WN071016 checked that _all_ Frontend/interface.sml uses this*)

fun term2xml j t = 

    indt (j+i) ^ "<MATHML>\n" ^ 

    indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^

    indt (j+i) ^ "</MATHML>";

(*val t = str2term "equality e_";

  writeln (term2xml 8 t);

          <MATHML>

            <ISA> equality e_ </ISA>

          <MATHML> *)

(*version for TextIO*)                                                         

fun terms2xml j [] = ""

  | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;

(*version for writeln: extra \n*)

fun terms2xml' j [] = ""

  | terms2xml' j [t] = term2xml j t

  | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;

(*WN060513 'cterm' means the Isabelle-type*)

fun cterm2xml j ct = 

    indt (j+i) ^ "<MATHML>\n" ^ 

    indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^

    indt (j+i) ^ "</MATHML>\n";

(*version for TextIO*)                                                         

fun cterms2xml j [] = ""

  | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;

(*version for writeln: extra \n*)

fun cterms2xml' j [] = ""

  | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;

(* writeln(cterms2xml 5 ["cterm1", "cterm2"]);

       <MATHML>

         <ISA> cterm1 </ISA>

       </MATHML>

       <MATHML>

         <ISA> cterm2 </ISA>

       </MATHML>

*)