(* convert sml-datatypes to xml for libisabelle and for kbase.

   authors: Walther Neuper 2003, 2016

   (c) due to copyright terms

*)

signature DATATYPES = (*TODO: redo with xml_of/to *)

  sig

    val authors2xml : int -> string -> string list -> xml

    val calc2xml : int -> ThyC.id * Rule_Def.calc -> xml

    val calcrefs2xml : int -> ThyC.id * Rule_Def.calc list -> xml

    val contthy2xml : int -> Thy_Present.contthy -> xml

    val extref2xml : int -> string -> string -> xml

    val filterpbl :

       ''a -> (''a * (Term.term * Term.term)) list -> Term.term list

    val formula2xml : int -> Term.term -> xml

    val formulae2xml : int -> Term.term list -> xml

    val i : int

    val id2xml : int -> string list -> string

    val ints2xml : int -> int list -> string

    val itm_2xml : int -> I_Model.feedback -> xml

    val itms2xml : int -> (int * Model_Def.variants * bool * string * I_Model.feedback) list ->

      string

    val keref2xml : int -> Specify.ketype -> Specify.kestoreID -> xml

    val model2xml :

       int -> I_Model.T -> (bool * Term.term) list -> xml

    val modspec2xml : int -> Ctree.ocalhd -> xml

    val pattern2xml :

       int ->

       (string * (Term.term * Term.term)) list -> Term.term list -> string

    val pos'2xml : int -> string * (int list * Pos.pos_) -> string

    val pos'calchead2xml : int -> Pos.pos' * Ctree.ocalhd -> xml

    val pos_2xml : int -> Pos.pos_ -> string

    val posform2xml : int -> Pos.pos' * Term.term -> xml

    val posformhead2xml : int -> Pos.pos' * Ctree.ptform -> string

    val posformheads2xml : int -> (Pos.pos' * Ctree.ptform) list -> xml

    val posforms2xml : int -> (Pos.pos' * Term.term) list -> xml

    val posterms2xml : int -> (Pos.pos' * term) list -> xml

    val precond2xml : int -> bool * Term.term -> xml

    val preconds2xml : int -> (bool * Term.term) list -> xml

    val rls2xml : int -> ThyC.id * Rule_Set.T -> xml

    val rule2xml : int -> Check_Unique.id -> Rule.rule -> xml

    val rules2xml : int -> Check_Unique.id -> Rule.rule list -> xml

    val scr2xml : int -> Program.T -> xml

    val spec2xml : int -> Spec.T -> xml

    val sub2xml : int -> Term.term * Term.term -> xml

    val subs2xml : int -> Subst.input -> xml

    val subst2xml : int -> subst -> xml

    val tac2xml : int -> Tactic.input -> xml

    val tacs2xml : int -> Tactic.input list -> xml

    val theref2xml : int -> ThyC.id -> string -> xstring -> string

    val thm''2xml : int -> thm -> xml

    val thmstr2xml : int -> string -> xml

  end

(*------------------------------------------------------------------

structure datatypes:DATATYPES =

(*structure datatypes =*)

struct

------------------------------------------------------------------*)

(*** convert sml-datatypes to xml for kbase ***)

(* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)

val i = indentation;

fun id2xml j ids =

    let fun id2x _ [] = ""

	  | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ 

			     (id2x j ss)

    in (indt j) ^ "<STRINGLIST>\n" ^ 

       (id2x (j + indentation) ids) ^ 

       (indt j) ^ "</STRINGLIST>\n" end;

(* writeln(id2xml 8 ["linear","univariate","equation"]);

        <STRINGLIST>

          <STRING>linear</STRING>

          <STRING>univariate</STRING>

          <STRING>equation</STRING>

        </STRINGLIST>*)

fun calc2xml j (thyID, (scrop, (rewop, _))) =

    indt j ^ "<CALC>\n" ^

    indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^

    indt (j+i) ^ "<GUH>\n" ^ Thy_Write.cal2guh ("IsacKnowledge", 

				      thyID) scrop  ^ "</GUH>\n" ^

    indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^

    indt j ^ "</CALC>\n";

(*replace by 'fun calc2xml' as developed for thy in 0607*)

fun calc2xmlOLD _ (scr_op, (isa_op, _)) =

    indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";

fun calcs2xmlOLD _ [] = "" (*TODO replace with 'strs2xml'*)

  | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;

(*.for creating a href for a rule within an rls's rule list;

   the guh points to the thy of definition of the rule, NOT of use in rls.*)

fun rule2xml _ _  Rule.Erule =

      error "rule2xml called with 'Erule'"

  | rule2xml j _ (Rule.Thm (thmDeriv, _)) =

      indt j ^ "<RULE>\n" ^

      indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^

      indt (j+i) ^ "<STRING> " ^ ThmC.cut_id thmDeriv ^ " </STRING>\n" ^

      indt (j+i) ^ "<GUH> " ^ 

        Thy_Write.thm2guh (Thy_Read.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^

        indt j ^ "</RULE>\n"

  | rule2xml _ _ (Rule.Eval (_(*termop*), _)) = ""

(*FIXXXXXXXME.WN060714 in rls make Eval : calc -> rule [add scriptop!]

  see smltest/../datatypes.sml !

    indt j ^ "<RULE>\n" ^

    indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^

    indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop) 

				    termop ^ " </GUH>\n" ^

    indt j ^ "</RULE>\n"

*)

  | rule2xml _ _ (Rule.Cal1 (_(*termop*), _)) = ""

  | rule2xml j thyID (Rule.Rls_ rls) =

      let val rls' = (#id o Rule_Set.rep) rls

      in

        indt j ^ "<RULE>\n" ^

        indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^

        indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^

        indt (j+i) ^ "<GUH> " ^ Thy_Write.rls2guh (Thy_Read.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^

        indt j ^ "</RULE>\n"

      end;

fun rules2xml _ _ [] = ""

  | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;

fun filterpbl str =

  let fun filt [] = []

        | filt ((s, (t1, t2)) :: ps) = 

	  if str = s then (t1 $ t2) :: filt ps else filt ps

  in filt end;

fun pattern2xml j p where_ =

    (case filterpbl "#Given" p of

	[] =>  (indt j) ^ "<GIVEN>  </GIVEN>\n"

(* val gis = filterpbl "#Given" p;

   *)

      | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^

	       (indt j) ^ "</GIVEN>\n")

    ^ 

    (case where_ of

	 [] =>  (indt j) ^ "<WHERE>  </WHERE>\n"

       | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^

		(indt j) ^ "</WHERE>\n")

    ^ 

    (case filterpbl "#Find" p of

	 [] =>  (indt j) ^ "<FIND>  </FIND>\n"

       | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^

		(indt j) ^ "</FIND>\n")

    ^ 

    (case filterpbl "#Relate" p of

	 [] =>  (indt j) ^ "<RELATE>  </RELATE>\n"

       | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^

		(indt j) ^ "</RELATE>\n");

(*

writeln(pattern2xml 3 ((#ppc o get_pbt)

			 ["squareroot","univariate","equation","test"]) []);

  *)

(*url to a source external to isac*)

fun extref2xml j linktext url =

    indt j ^ "<EXTREF>\n" ^

    indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^

    indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^

    indt j ^ "</EXTREF>\n";

fun theref2xml j thyID typ xstring =

    let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]

	val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ

    in indt j ^ "<KESTOREREF>\n" ^

       indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^

       indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^

       indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^

       indt j ^ "</KESTOREREF>\n"

    end;

fun keref2xml j typ kestoreID =

    let val id = strs2str' kestoreID

	val guh = Specify.kestoreID2guh typ kestoreID

    in indt j ^ "<KESTOREREF>\n" ^

       indt (j+i) ^ "<TAG> " ^ Specify.ketype2str' typ ^ "</TAG>\n" ^

       indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^

       indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^

       indt j ^ "</KESTOREREF>\n"

    end;

fun authors2xml j str auts = 

    let fun autx _ [] = ""

	  | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ 

			     (autx j ss)

    in indt j ^ "<"^str^">\n" ^

       autx (j + i) auts ^ 

       indt j ^ "</"^str^">\n"

    end;

(* writeln(authors2xml 2 "MATHAUTHORS" []);

   writeln(authors2xml 2 "MATHAUTHORS" 

		       ["isac-team 2001", "Richard Lang 2003"]);

   *)

fun scr2xml j Rule.Empty_Prog =

    indt j ^"<SCRIPT>  </SCRIPT>\n"

  | scr2xml j (Rule.Prog term) =

    if term = TermC.empty 

    then indt j ^"<SCRIPT>  </SCRIPT>\n"

    else indt j ^"<SCRIPT>\n"^ 

	 term2xml j (TermC.inst_abs term) ^ "\n" ^

	 indt j ^"</SCRIPT>\n"

  | scr2xml j (Rule.Rfuns _) =

    indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";

fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =

    indt j ^ "<CALCREF>\n" ^

    indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^

    indt (j+i) ^ "<GUH> " ^ Thy_Write.cal2guh ("IsacKnowledge", 

				      thyID) scrop  ^ " </GUH>\n" ^

    indt j ^ "</CALCREF>\n";

fun calcrefs2xml _ (_,[]) = ""

  | calcrefs2xml j (thyID, cal::cs) = 

    calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);

fun prepa12xml j (terms, term) =

    indt j ^"<PREPAT>\n"^

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

    terms2xml (j+2*i) terms ^

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

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

    term2xml (j+2*i) term ^

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

    indt j ^"</PREPAT>\n";

fun prepat2xml _ [] = ""

  | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;

fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

		      srls, calc, rules, errpatts, scr}) =

    indt j ^"<RULESET>\n"^

    indt (j+i) ^"<ID> "^ id ^" </ID>\n"^

    indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^

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

    rules2xml (j+2*i) thyID rules ^

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

    indt (j+i) ^"<PRECONDS> " ^

    terms2xml' (j+2*i) preconds ^

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

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

    indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^

(*WN060714 thy_isac_*-ord-*.xml not yet generated ................

    indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", 

				      thyID) ord ^ " </GUH>\n" ^

..................................................................*)

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

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

    indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^

    indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID) 

				     (Rule_Set.id erls) ^ " </GUH>\n" ^

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

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

    indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^

    indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID) 

				     (Rule_Set.id srls) ^ " </GUH>\n" ^

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

    calcrefs2xml (j+i) (thyID, calc) ^

    scr2xml (j+i) scr ^

    indt j ^"</RULESET>\n";

fun rls2xml j (thyID, Rule_Set.Empty) = rls2xml j (thyID, Rule_Set.empty)

  | rls2xml j (thyID, Rule_Def.Repeat data) = rls2xm j (thyID, "Rls", data)

  | rls2xml j (thyID, Rule_Set.Sequence data) = rls2xm j (thyID, "Seq", data)

  | rls2xml j (thyID, Rule_Set.Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) = 

    indt j ^"<RULESET>\n"^

    indt (j+i) ^"<ID> "^ id ^" </ID>\n"^

    indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^

    prepat2xml (j+i) prepat ^

    indt (j+i) ^"<ORDER> " ^

    indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^

(*WN060714 thy_isac_*-ord-*.xml not yet generated ................

    indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", 

				      thyID) ord ^ " </GUH>\n" ^

.................................................................*)

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

    indt (j+i) ^"<ERLS> " ^

    indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^

    indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^

    indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id erls) ^ " </GUH>\n" ^

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

    calcrefs2xml (j+i) (thyID, calc) ^

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

    scr2xml (j+2*i) scr ^

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

    indt j ^"</RULESET>\n";

(*** convert sml-datatypes to xml for libisabelle ***)

(** general types: lists,  **)

fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])

fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b

  | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = Specify.str2ketype' str

  | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])

fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)

fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str

  | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs

  | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])

fun xml_of_ints is =

  XML.Elem (("INTLIST", []), map xml_of_int is)

fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) = 

      (case TermC.int_opt_of_string i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")

  | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is

  | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)

(** isac datatypes **)

fun xml_of_pos tag (is, pp) =

  XML.Elem ((tag, []), [

    xml_of_ints is,

    XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])

fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = Pos.str2pos_ pp

  | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)

  | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_of_auto (Solve.Steps i) = 

      XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])

  | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])

  | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])

  | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])

  | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])

  | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])

fun xml_to_auto (XML.Elem (("AUTO", []), [

      XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Steps (TermC.int_opt_of_string i |> the)

  | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel

  | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = Solve.CompleteCalcHead

  | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = Solve.CompleteToSubpbl

  | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl

  | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc

  | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)

fun filterpbl str =

  let fun filt [] = []

        | filt ((s, (t1, t2)) :: ps) = 

	  if str = s then (t1 $ t2) :: filt ps else filt ps

  in filt end;

fun xml_of_itm_ (I_Model.Cor (dts, _)) =

    XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (O_Model.comp_dts' dts)])

  | xml_of_itm_ (I_Model.Syn c) =

    XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])

  | xml_of_itm_ (I_Model.Typ c) =

    XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])

  (*type item also has 'False of cterm' set in preconds2xml WN 050618*)

  | xml_of_itm_ (I_Model.Inc (dts, _)) = 

    XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (O_Model.comp_dts' dts)])

  | xml_of_itm_ (I_Model.Sup dts) = 

    XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (O_Model.comp_dts' dts)])

  | xml_of_itm_ (I_Model.Mis (d, pid)) = 

    XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])

  | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"

fun xml_of_itms itms =

  let 

    fun extract (_, _, _, _, itm_) = itm_

      | extract _ = error "xml_of_itms.extract: wrong argument" 

  in map (xml_of_itm_ o extract) itms end

fun xml_of_precond (status, term) =

    XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])

fun xml_of_preconds ps = map xml_of_precond ps

fun xml_of_model itms where_ =

  let

    fun eq str (_, _, _,field, _) = str = field

  in 

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

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

        filter (eq "#Given") itms |> xml_of_itms),

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

        xml_of_preconds where_),

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

        filter (eq "#Find") itms |> xml_of_itms),

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

        filter (eq "#Relate") itms |> xml_of_itms)])

  end 

fun xml_of_spec (thyID, pblID, metID) =

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

    XML.Elem (("THEORYID", []), [XML.Text thyID]),

    XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),

    XML.Elem (("METHODID", []), [xml_of_strs metID])])

fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [

      XML.Elem (("THEORYID", []), [XML.Text thyID]),

      XML.Elem (("PROBLEMID", []), [ps]),

      XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)

  | xml_to_spec tree = raise ERROR ("xml_to_spec: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_of_variant (items, spec) = 

  XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])

fun xml_to_variant (XML.Elem (("VARIANT", []), [items, spec])) = 

    (xml_to_strs items, xml_to_spec spec)

  | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]

  | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)

fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars

  | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)

fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Ctree.ocalhd) =

  XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [

    XML.Elem (("HEAD", []), [xml_of_term_NEW head]),

    xml_of_model gfr pre,

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

      XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),

    xml_of_spec spec])

fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): Ctree.ocalhd)) =

  XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [

    xml_of_pos "POSITION" p,

    XML.Elem (("HEAD", []), [xml_of_term_NEW head]),

    xml_of_model gfr pre,

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

      XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),

    xml_of_spec spec])

fun xml_to_imodel

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

      XML.Elem (("GIVEN", []), givens),

      (*XML.Elem (("WHERE", []), wheres),  ... Where is never input*)

      XML.Elem (("FIND", []), finds),

      XML.Elem (("RELATE", []), relates)])) =

    ([In_Chead.Given (map xml_to_cterm givens), 

      In_Chead.Find (map xml_to_cterm finds), 

      In_Chead.Relate (map xml_to_cterm relates)]) : In_Chead.imodel

  | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)

fun xml_to_icalhd

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

      pos as XML.Elem ((   "POSITION", []), _),

      XML.Elem ((          "HEAD", []), [form]),

      imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)

      XML.Elem ((          "POS", []), [XML.Text belongsto]),

      spec as XML.Elem ((  "SPECIFICATION", []), _)])) =

    (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel, 

    Pos.str2pos_ belongsto, xml_to_spec spec) : In_Chead.icalhd

  | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)

fun xml_of_sub (id, value) =

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

    XML.Elem (("VARIABLE", []), [xml_of_term id]),

    XML.Elem (("VALUE", []), [xml_of_term value])])

fun xml_to_sub

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

      XML.Elem (("VARIABLE", []), [id]),

      XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)

  | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)

fun xml_of_subs (subs : Subst.input) =

  XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs))

fun xml_to_subs

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

      subs)) = Subst.T_to_input (map xml_to_sub subs)

  | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)

fun xml_of_sube sube =

  XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))

fun xml_to_sube

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

      xml_var_val_pairs)) = Subst.T_to_string_eqs (map xml_to_sub xml_var_val_pairs)

  | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)

fun thm''2xml j (thm : thm) =

    indt j ^ "<THEOREM>\n" ^

    indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^

    term2xml j (Thm.prop_of thm) ^ "\n" ^

    indt j ^ "</THEOREM>\n";

fun xml_of_thm' (ID, form) =

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

    XML.Elem (("ID", []), [XML.Text ID]),

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

      XML.Text form])])           (* repair for MathML: use term instead String *)

(* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)

fun xml_of_thm'' (ID, thm) =

(*---xml_of_thm''------------------------------------------thm'_to_thm''--------------

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

    XML.Elem (("ID", []), [XML.Text ID]),

    xml_of_term_NEW term])

-----xml_of_thm''------------------------------------------thm'_to_thm''------------*)

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

    XML.Elem (("ID", []), [XML.Text ID]),

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

      XML.Text ((UnparseC.term o Thm.prop_of) thm)])])           (* repair for MathML: use term instead String *)

fun xml_to_thm'

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

      XML.Elem (("ID", []), [XML.Text ID]),

      XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) =

    (ID, "NO_ad_hoc_thm_FROM_GUI = True")

  | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:\n" ^ xmlstr 0 x)

(* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)

fun xml_to_thm''

(*---xml_of_thm''------------------------------------------thm'_to_thm''--------------

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

      XML.Elem (("ID", []), [XML.Text ID]),

      xterm])) =

    (ID, xml_to_term_NEW xterm) : thm''

  | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x)

-----xml_of_thm''------------------------------------------thm'_to_thm''------------*)

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

      XML.Elem (("ID", []), [XML.Text ID]),

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

        XML.Text term])])) = (ID, ThmC.thm_from_thy (ThyC.Isac ()) ID)

  | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)

fun xml_of_src Rule.Empty_Prog =

    XML.Elem (("NOCODE", []), [XML.Text "empty"])

  | xml_of_src (Rule.Prog term) =

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

      if term = TermC.empty then xml_of_src Rule.Empty_Prog

      else xml_of_term (TermC.inst_abs term)])

  | xml_of_src (Rule.Rfuns _) =

    XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])

(*.convert a tactic into xml-format .*)

fun xml_of_tac (Tactic.Subproblem (dI, pI)) =

    XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [

      XML.Elem (("THEORY", []), [XML.Text dI]),

      XML.Elem (("PROBLEM", []), [xml_of_strs pI])])

  | xml_of_tac (Tactic.Substitute cterms) =

    (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)

    XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])

    (*----- Rewrite* -----------------------------------------------------*)

  | xml_of_tac (Tactic.Rewrite thm'') =

    XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])

  | xml_of_tac (Tactic.Rewrite_Inst (subs, thm'')) =

    XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (

      xml_of_subs subs ::

      xml_of_thm'' thm'' :: []))

  | xml_of_tac (Tactic.Rewrite_Set rls') =

    XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])

  | xml_of_tac (Tactic.Rewrite_Set_Inst (subs, rls')) =

    XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([

      xml_of_subs subs,

      XML.Elem (("RULESET", []), [XML.Text rls'])]))

    (*----- FORMTACTIC ---------------------------------------------------*)

  | xml_of_tac (Tactic.Add_Find ct) =

    XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Add_Given ct) =

    XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Add_Relation ct) =

    XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Check_elementwise ct) =

    XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Take ct) =

    XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])

    (*----- SIMPLETACTIC -------------------------------------------------*)

  | xml_of_tac (Tactic.Calculate opstr) =

    XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])

  | xml_of_tac (Tactic.Or_to_List) =

    XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])

  | xml_of_tac (Tactic.Specify_Theory ct) =

    XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])

    (*----- STRINGLISTTACTIC ---------------------------------------------*)

  | xml_of_tac (Tactic.Apply_Method mI) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])

  | xml_of_tac (Tactic.Check_Postcond pI) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])

  | xml_of_tac Model_Problem =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])

  | xml_of_tac (Tactic.Refine_Tacitly pI) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])

  | xml_of_tac (Tactic.Specify_Method ct) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])

  | xml_of_tac (Tactic.Specify_Problem ct) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])

  | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);

fun xml_to_tac 

    (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [

      XML.Elem (("THEORY", []), [XML.Text dI]),

      XML.Elem (("PROBLEM", []), [pI])])) = Tactic.Subproblem (dI, xml_to_strs pI)

  | xml_to_tac

    (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Substitute")]), [cterms])) = Tactic.Substitute (xml_to_sube cterms)

    (*----- Rewrite* -----------------------------------------------------*)

  | xml_to_tac

    (XML.Elem (("REWRITETACTIC", [

      ("name", "Rewrite")]), [thm])) = Tactic.Rewrite (xml_to_thm'' thm)

  | xml_to_tac

    (XML.Elem (("REWRITEINSTTACTIC", [

      ("name", "Rewrite_Inst")]), [

        subs, thm])) = Tactic.Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)

  | xml_to_tac

    (XML.Elem (("REWRITESETTACTIC", [

      ("name", "Rewrite_Set")]), [XML.Text rls'])) = Tactic.Rewrite_Set (rls')

  | xml_to_tac

    (XML.Elem (("REWRITESETINSTTACTIC", [

      ("name", "Rewrite_Set_Inst")]), [

        subs,

        XML.Elem (("RULESET", []), [XML.Text rls'])])) = Tactic.Rewrite_Set_Inst (xml_to_subs subs, rls')

    (*----- FORMTACTIC ---------------------------------------------------*)

  | xml_to_tac

    (XML.Elem (("FORMTACTIC", [

      ("name", "Add_Find")]), [ct])) =  Tactic.Add_Find (xml_to_cterm ct)

  | xml_to_tac

    (XML.Elem (("FORMTACTIC", [

      ("name", "Add_Given")]), [ct])) = Tactic.Add_Given (xml_to_cterm ct)

  | xml_to_tac

    (XML.Elem (("FORMTACTIC", [

      ("name", "Add_Relation")]), [ct])) = Tactic.Add_Relation (xml_to_cterm ct)

  | xml_to_tac

    (XML.Elem (("FORMTACTIC", [

      ("name", "Take")]), [ct])) = Tactic.Take (xml_to_cterm ct)

  | xml_to_tac

    (XML.Elem (("FORMTACTIC", [

      ("name", "Check_elementwise")]), [ct])) = Tactic.Check_elementwise (xml_to_cterm ct)

    (*----- SIMPLETACTIC -------------------------------------------------*)

  | xml_to_tac

    (XML.Elem (("SIMPLETACTIC", [

      ("name", "Calculate")]), [XML.Text opstr])) = Tactic.Calculate opstr

  | xml_to_tac

    (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Tactic.Or_to_List

  | xml_to_tac

    (XML.Elem (("SIMPLETACTIC", [

      ("name", "Specify_Theory")]), [XML.Text ct])) = Tactic.Specify_Theory ct

    (*----- STRINGLISTTACTIC ---------------------------------------------*)

  | xml_to_tac

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Apply_Method")]), [mI])) = Tactic.Apply_Method (xml_to_strs  mI)

  | xml_to_tac

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Check_Postcond")]), [pI])) = Tactic.Check_Postcond (xml_to_strs pI)

  | xml_to_tac

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Model_Problem")]), [])) = Tactic.Model_Problem 

  | xml_to_tac

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Refine_Tacitly")]), [pI])) = Tactic.Refine_Tacitly (xml_to_strs pI)

  | xml_to_tac

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Specify_Method")]), [ct])) = Tactic.Specify_Method (xml_to_strs ct)

  | xml_to_tac

    (XML.Elem (("STRINGLISTTACTIC", [

      ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct)

  | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);

val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) 

		    ("Problem (" ^ ThyC.id_empty ^ "," ^ strs2str' Problem.id_empty ^ ")");

(*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)

fun xml_of_posterm (p, t, _) =

  let val input_request = Free ("________________________________________________", dummyT)

  in 

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

      [xml_of_pos "POSITION" p,

       if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)

       then xml_of_term_NEW input_request

       else xml_of_term_NEW t])

  end

fun xml_of_asm_val (asm, vl) =

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

    XML.Elem (("ASM", []), [xml_of_term asm]),

    XML.Elem (("VALUE", []), [xml_of_term vl])])

(*.a reference to an element in the theory hierarchy; 

   compare 'fun keref2xml'.*)

(* val (j, thyID, typ, xstring) = 

       (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');

   *)

fun theref2xml j thyID typ xstring =

    let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]

	val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ

    in indt j ^ "<KESTOREREF>\n" ^

       indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^

       indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^

       indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^

       indt j ^ "</KESTOREREF>\n"

    end;

fun xml_of_theref thyid typ xstring =

  let 

    val guh = Thy_Write.theID2guh ["IsacKnowledge", thyid, typ, xstring]

    val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ

  in 

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

      XML.Elem (("TAG", []), [XML.Text typ']),

      XML.Elem (("ID", []), [XML.Text xstring]),

      XML.Elem (("GUH", []), [XML.Text guh])])

  end

fun xml_of_contthy Thy_Present.EContThy =

    error "contthy2xml called with EContThy"

  | xml_of_contthy (Thy_Present.ContThm {thyID, thm, applto, applat, reword, 

				asms,lhs, rhs, result, resasms, asmrls}) =

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

      XML.Elem (("GUH", []), [XML.Text thm]),

      XML.Elem (("APPLTO", []), [xml_of_term applto]),

      XML.Elem (("APPLAT", []), [xml_of_term applat]),

      XML.Elem (("ORDER", []), [ (* should be a theref2xml *)

        XML.Elem (("ID", []), [XML.Text reword])]),

      XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),

      XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),

      XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),

      XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),

      XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),

      XML.Elem (("RESULT", []), [xml_of_term result]),

      XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),

      XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])

  | xml_of_contthy (Thy_Present.ContThmInst {thyID, thm, bdvs, thminst, applto, applat, 

				reword, asms, lhs, rhs, result, resasms, asmrls}) =

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

      XML.Elem (("GUH", []), [XML.Text thm]),

      XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)

        xml_of_cterm (Env.subst2str' bdvs)]),

      XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),

      XML.Elem (("APPLTO", []), [xml_of_term applto]),

      XML.Elem (("APPLAT", []), [xml_of_term applat]),

      XML.Elem (("ORDER", []), [ (* should be a theref2xml *)

        XML.Elem (("ID", []), [XML.Text reword])]),

      XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),

      XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),

      XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),

      XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),

      XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),

      XML.Elem (("RESULT", []), [xml_of_term result]),

      XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),

      XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])

  | xml_of_contthy (Thy_Present.ContRls {thyID = _, rls, applto, result, asms}) =

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

      XML.Elem (("GUH", []), [XML.Text rls]),

      XML.Elem (("APPLTO", []), [xml_of_term applto]),

      XML.Elem (("RESULT", []), [xml_of_term result]),

      XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])

  | xml_of_contthy (Thy_Present.ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =

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

      XML.Elem (("GUH", []), [XML.Text rls]),

      XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)

        xml_of_cterm (Env.subst2str' bdvs)]),

      XML.Elem (("INSTANTIATED", []), [xml_of_cterm (Env.subst2str' bdvs)]),

      XML.Elem (("APPLTO", []), [xml_of_term applto]),

      XML.Elem (("RESULT", []), [xml_of_term result]),

      XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])

  | xml_of_contthy (Thy_Present.ContNOrew {thyID = _, thm_rls, applto}) =

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

      XML.Elem (("GUH", []), [XML.Text thm_rls]),

      XML.Elem (("APPLTO", []), [xml_of_term applto])])

  | xml_of_contthy (Thy_Present.ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =

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

      XML.Elem (("GUH", []), [XML.Text thm_rls]),

      XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)

        xml_of_cterm (Env.subst2str' bdvs)]),

      XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),

      XML.Elem (("APPLTO", []), [xml_of_term applto])])

fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =

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

    XML.Elem (("GUH", []), [XML.Text (Specify.pblID2guh pI)]),

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

      XML.Text ((if model_ok then "correct" else "incorrect"))]),

    XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),

    xml_of_model pbl pre])

fun xml_of_matchmet (model_ok, pI, scr, pbl, pre) =

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

    XML.Elem (("GUH", []), [XML.Text (Specify.metID2guh pI)]),

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

      XML.Text ((if model_ok then "correct" else "incorrect"))]),

    XML.Elem (("PROGRAM", []), [xml_of_src scr]),

    xml_of_model pbl pre])

fun xml_of_calcchanged calcid tag old del new =

  (*TODO: make analogous to xml_to_calcchanged*)

  XML.Elem ((tag, []),[

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

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

      xml_of_pos "UNCHANGED" old,

      xml_of_pos "DELETED" del,

      xml_of_pos "GENERATED" new])])

fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) = 

      (xml_to_pos old, xml_to_pos del, xml_to_pos new)

  | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)

(* for checking output at Frontend *)

fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode

(*------------------------------------------------------------------

end

open datatypes;

------------------------------------------------------------------*)