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

   author: Walther Neuper 030701

   (c) isac-team 2003

This code remains in order to

keep tests of interaction Java-frontend <-> Kernel running.

*)

val indentation = 2;

(*

   EXCEPT xml-coding issues (2).

   (2) have a _reverse_ method 

   'isac.util.parser.FormalizationDigest.decodeEntities' 

   called within Formula#toSMLString in java

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

         decode "&" ---> "&"

   called for term2xml; + see "fun encode" below*)

fun decode (str: TermC.as_string) = 

    let fun dec [] = []

	  | 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 Symbol.explode) str: TermC.as_string end;

fun dop_leading _ [] = []

  | dop_leading c (c' :: cs) =

    if c = c' then dop_leading c cs else (c' :: cs)

fun rm_doublets _ singled [] = singled

  | rm_doublets c singled (c' :: cs) =

    if c = c'

    then 

      let val cs' = dop_leading "^" cs

      in rm_doublets c (singled @ [c']) cs' end

    else rm_doublets c (singled @ [c']) cs

fun encode (str : TermC.as_string) =

    let fun enc [] = []

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

	  | enc (c :: cs) = c :: (enc cs)

    in str |> Symbol.explode |> rm_doublets "^" [] |>  enc |>  implode end;

val i = indentation;

(* proper <> is translated to html; however, () creates readable output.. *)

fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"

  | xmlstr i (XML.Elem (("TERM", []), [_])) = 

    indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^

    indent (i + 1) ^ "rm libisabelle: xt NOT DECODED" ^ "\n" ^

    indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"

  | xmlstr i (XML.Elem ((str, []), trees)) = 

    indent i ^ "(" ^ str ^ ")" ^ "\n" ^

      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^

    indent i ^ "(/" ^ str ^ ")" ^ "\n"

  | xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) = 

    indent i ^ "(" ^ str ^ " " ^ flag ^ "=" ^ value  ^ ")" ^ "\n" ^

      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^

    indent i ^ "(/" ^ str ^ ")" ^ "\n"

  | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) = 

    raise ERROR "xmlstr: TODO review attribute \"status\" etc";

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

(*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 UnparseC.term) t ^ " </ISA>\n" ^

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

(*val t = TermC.parse_test @{context} "equality e_";

  writeln (term2xml 8 t);

          <MATHML>

            <ISA> equality e_ </ISA>

          <MATHML> *)

fun xml_of_term t =

  XML.Elem (("MATHML", []),

    [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])])

fun xml_of_terms ts = map xml_of_term ts

(* intermediate replacements while introducing transfer of terms by libisabelle *)

fun xml_of_term_NEW (t : term) =

  XML.Elem (("FORMULA", []), [

    XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)]),

    XML.Text ("(TERM)\n " ^ UnparseC.term t  ^ "\n(/TERM)")

    ])

(*version for TextIO*)                                                         

fun terms2xml _ [] = ""

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

(*version for writeln: extra \n*)

fun terms2xml' _ [] = ""

  | 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";

fun xml_of_cterm ct = 

  XML.Elem (("MATHML", []),

    [XML.Elem (("ISA", []), [XML.Text ct])])

(*version for TextIO*)                                                         

fun cterms2xml _ [] = ""

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

(*version for writeln: extra \n*)

fun cterms2xml' _ [] = ""

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