1.1 --- a/src/Tools/isac/Frontend/interface.sml	Sun Aug 09 10:00:11 2015 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Sun Aug 09 15:15:01 2015 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4      val setProblem : calcID -> pblID -> XML.tree
     1.5      val setTheory : calcID -> thyID -> XML.tree
     1.6  (*------------ for tests*)
     1.7 -val encode: cterm' -> cterm'
     1.8 +(*val encode: cterm' -> cterm'   GONE TO xmlsrc/mathml.sml*)
     1.9  val encode_fmz: fmz -> fmz
    1.10    end
    1.11  
    1.12 @@ -71,12 +71,7 @@
    1.13     format accepted by Isabelle.
    1.14     encode "^" ---> "^^^"; see Knowledge/Atools.thy;
    1.15     called for each cterm', icalhd, fmz in this interface;
    1.16 -   + see "fun decode" in xmlsrc/mathml.sml *)
    1.17 -fun encode (str : cterm') =
    1.18 -    let fun enc [] = []
    1.19 -	  | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
    1.20 -	  | enc (c :: cs) = c :: (enc cs)
    1.21 -    in (implode o enc o Symbol.explode) str:cterm' end;
    1.22 +   + see "fun en/decode" in xmlsrc/mathml.sml *)
    1.23  fun encode_imodel (imodel:imodel) =
    1.24      let fun enc (Given ifos) = Given (map encode ifos)
    1.25  	  | enc (Find ifos) = Find (map encode ifos)

     2.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Sun Aug 09 10:00:11 2015 +0200
     2.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Sun Aug 09 15:15:01 2015 +0200
     2.3 @@ -67,24 +67,6 @@
     2.4  struct
     2.5  ------------------------------------------------------------------*)
     2.6  
     2.7 -val i = indentation;
     2.8 -
     2.9 -local
    2.10 -fun indent i = fold (curry op ^) (replicate i ". ") ""
    2.11 -in
    2.12 -fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
    2.13 -  | xmlstr i (XML.Elem ((str, []), trees)) = 
    2.14 -    indent i ^ "<" ^ str ^ ">" ^ "\n" ^
    2.15 -      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
    2.16 -    indent i ^ "</" ^ str ^ ">" ^ "\n"
    2.17 -  | xmlstr i (XML.Elem ((str, [("status", a)]), trees)) = 
    2.18 -    indent i ^ "<" ^ str ^ " status " ^ a  ^ ">" ^ "\n" ^
    2.19 -      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
    2.20 -    indent i ^ "</" ^ str ^ ">" ^ "\n"
    2.21 -  | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) = 
    2.22 -    error "xmlstr: TODO review attribute \"status\" etc";
    2.23 -end
    2.24 -
    2.25  (** general types: lists,  **)
    2.26  
    2.27  fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
    2.28 @@ -192,6 +174,11 @@
    2.29  fun xml_of_formula term = 
    2.30    XML.Elem (("FORMULA", []), [
    2.31      XML.Elem (("CALCID", []), [xml_of_term term])])
    2.32 +fun xml_to_formula 
    2.33 +      (XML.Elem (("FORMULA", []), [
    2.34 +        XML.Elem (("CALCID", []), [form])])) = xml_to_term form
    2.35 +  | xml_to_formula x = raise ERROR ("xml_to_formulax wrong arg: " ^ xmlstr 0 x)
    2.36 +(* TODO test/Tools/isac/xmlsrc/datatypes.sml*)
    2.37  
    2.38  fun formulae2xml j [] = ("":xml)
    2.39    | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;

     3.1 --- a/src/Tools/isac/xmlsrc/mathml.sml	Sun Aug 09 10:00:11 2015 +0200
     3.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml	Sun Aug 09 15:15:01 2015 +0200
     3.3 @@ -2,9 +2,6 @@
     3.4     TODO implement MathML
     3.5     author: Walther Neuper 030701
     3.6     (c) isac-team 2003
     3.7 -
     3.8 -use"xmlsrc/mathml.sml";
     3.9 -use"mathml.sml";
    3.10  *)
    3.11  
    3.12  (*.decode Isabelle-strings to the format as seen by the user (1)
    3.13 @@ -25,7 +22,29 @@
    3.14  	  | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
    3.15  	  | dec (c::cs) = c::(dec cs)
    3.16      in (implode o dec o Symbol.explode) str:cterm' end;
    3.17 +fun encode (str : cterm') =
    3.18 +    let fun enc [] = []
    3.19 +	  | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
    3.20 +	  | enc (c :: cs) = c :: (enc cs)
    3.21 +    in (implode o enc o Symbol.explode) str:cterm' end;
    3.22  
    3.23 +val indentation = 2;
    3.24 +
    3.25 +local
    3.26 +fun indent i = fold (curry op ^) (replicate i ". ") ""
    3.27 +in
    3.28 +fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
    3.29 +  | xmlstr i (XML.Elem ((str, []), trees)) = 
    3.30 +    indent i ^ "<" ^ str ^ ">" ^ "\n" ^
    3.31 +      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
    3.32 +    indent i ^ "</" ^ str ^ ">" ^ "\n"
    3.33 +  | xmlstr i (XML.Elem ((str, [("status", a)]), trees)) = 
    3.34 +    indent i ^ "<" ^ str ^ " status " ^ a  ^ ">" ^ "\n" ^
    3.35 +      List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
    3.36 +    indent i ^ "</" ^ str ^ ">" ^ "\n"
    3.37 +  | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) = 
    3.38 +    error "xmlstr: TODO review attribute \"status\" etc";
    3.39 +end
    3.40  
    3.41  fun strs2xml strs = foldl (op ^) ("", strs); 
    3.42  (* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
    3.43 @@ -49,6 +68,12 @@
    3.44    XML.Elem (("MATHML", []),
    3.45      [XML.Elem (("ISA", []), [XML.Text ((decode o term2str) t)])])
    3.46  fun xml_of_terms ts = map xml_of_term ts
    3.47 +fun xml_to_term 
    3.48 +      ((XML.Elem (("MATHML", []), [
    3.49 +        XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> str2term
    3.50 +  | xml_to_term xx = raise ERROR ("xml_to_term wrong arg: " ^ xmlstr 0 xx)
    3.51 +fun xml_to_terms ts = map xml_to_term ts
    3.52 +(* TODO test/Tools/isac/xmlsrc/mathml.sml*)
    3.53  
    3.54  (*version for TextIO*)                                                         
    3.55  fun terms2xml j [] = ""