1.1 --- a/src/Tools/isac/calcelems.sml	Tue Jun 09 09:41:53 2015 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Jun 17 15:46:55 2015 +0200
     1.3 @@ -49,7 +49,10 @@
     1.4  type guh = string;
     1.5  val e_guh = "e_guh":guh;
     1.6  
     1.7 -type xml = string;
     1.8 +type xml = string; (* rm together with old code replaced by XML.tree *)
     1.9 +fun string_to_bool "true" = true
    1.10 +  | string_to_bool "false" = false
    1.11 +  | string_to_bool str = error ("string_to_bool: arg = " ^ str)
    1.12  
    1.13  (* eval function calling sml code during rewriting.
    1.14  Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,

     2.1 --- a/src/Tools/isac/library.sml	Tue Jun 09 09:41:53 2015 +0200
     2.2 +++ b/src/Tools/isac/library.sml	Wed Jun 17 15:46:55 2015 +0200
     2.3 @@ -321,8 +321,7 @@
     2.4  (*fun indt 0 = ""
     2.5    | indt n = " " ^ indt (n-1);---------does not terminate with negatives*)
     2.6  fun indt n = if n <= 0 then "" else " " ^ indt (n-1);
     2.7 -fun indent 0 = ""
     2.8 -  | indent n = ". " ^ indent(n-1);
     2.9 +fun indent i = fold (curry op ^) (replicate i ". ") ""
    2.10  
    2.11  fun dashs i = if 0<i then "-"^ dashs (i-1) else "";
    2.12  fun dots i = if 0<i then "."^ dots (i-1) else "";

     3.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Tue Jun 09 09:41:53 2015 +0200
     3.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Wed Jun 17 15:46:55 2015 +0200
     3.3 @@ -89,7 +89,7 @@
     3.4  
     3.5  fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
     3.6  fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
     3.7 -  | xml_to_bool tree = error ("xml_to_int: wrong XML.tree " ^ xmlstr 0 tree)
     3.8 +  | xml_to_bool tree = error ("xml_to_bool: wrong XML.tree " ^ xmlstr 0 tree)
     3.9  
    3.10  (*.handles string list like 'fun id2xml'.*)
    3.11  fun authors2xml j str auts = 
    3.12 @@ -165,7 +165,6 @@
    3.13    XML.Elem ((tag, []), [
    3.14      xml_of_ints is,
    3.15      XML.Elem (("POS", []), [XML.Text (pos_2str pp)])])
    3.16 -
    3.17  fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = str2pos_ pp
    3.18    | xml_to_pos_ tree = error ("xml_to_pos_: wrong XML.tree " ^ xmlstr 0 tree)
    3.19  fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
    3.20 @@ -429,10 +428,18 @@
    3.21      XML.Elem (("METHODID", []), [xml_of_strs metID])])
    3.22  fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
    3.23        XML.Elem (("THEORYID", []), [XML.Text thyID]),
    3.24 -      XML.Elem (("PROBLEMID", []), ps),
    3.25 -      XML.Elem (("METHODID", []), ms)])) = (thyID, map xml_to_strs ps, map xml_to_strs ms)
    3.26 +      XML.Elem (("PROBLEMID", []), [ps]),
    3.27 +      XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)
    3.28    | xml_to_spec tree = error ("xml_to_spec: wrong XML.tree " ^ xmlstr 0 tree)
    3.29  
    3.30 +fun xml_of_fmz [] = xml_of_fmz [e_fmz]
    3.31 +  | xml_of_fmz [(items, spec)] = 
    3.32 +    XML.Elem (("FORMALIZATION", []), [xml_of_strs items, xml_of_spec spec])
    3.33 +  | xml_of_fmz (_ :: _) = error "xml_of_fmz: expect single (still?)"
    3.34 +fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), [its, spc])) =
    3.35 +    [(xml_to_strs its, xml_to_spec spc)]
    3.36 +  | xml_to_fmz tree = error ("xml_to_fmz: wrong XML.tree " ^ xmlstr 0 tree)
    3.37 +
    3.38  fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =
    3.39      (indt j ^"<CALCHEAD status = "^
    3.40       quote (if b then "correct" else "incorrect")^">\n"^