1 (* translate formulae from Isabelle-string format to xml-format.
2 author: Walther Neuper 030701
5 This code remains in order to
6 keep tests of interaction Java-frontend <-> Kernel running.
12 EXCEPT xml-coding issues (2).
13 (2) have a _reverse_ method
14 'isac.util.parser.FormalizationDigest.decodeEntities'
15 called within Formula#toSMLString in java
17 ad(2) decode "<" ---> "<", decode ">" ---> ">"
18 decode "&" ---> "&"
19 called for term2xml; + see "fun encode" below*)
20 fun decode (str: TermC.as_string) =
22 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
23 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
24 | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
25 | dec (c::cs) = c::(dec cs)
26 in (implode o dec o Symbol.explode) str: TermC.as_string end;
28 fun dop_leading _ [] = []
29 | dop_leading c (c' :: cs) =
30 if c = c' then dop_leading c cs else (c' :: cs)
31 fun rm_doublets _ singled [] = singled
32 | rm_doublets c singled (c' :: cs) =
35 let val cs' = dop_leading "^" cs
36 in rm_doublets c (singled @ [c']) cs' end
37 else rm_doublets c (singled @ [c']) cs
38 fun encode (str : TermC.as_string) =
40 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
41 | enc (c :: cs) = c :: (enc cs)
42 in str |> Symbol.explode |> rm_doublets "^" [] |> enc |> implode end;
46 (* proper <> is translated to html; however, () creates readable output.. *)
47 fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
48 | xmlstr i (XML.Elem (("TERM", []), [_])) =
49 indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^
50 indent (i + 1) ^ "rm libisabelle: xt NOT DECODED" ^ "\n" ^
51 indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"
52 | xmlstr i (XML.Elem ((str, []), trees)) =
53 indent i ^ "(" ^ str ^ ")" ^ "\n" ^
54 List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
55 indent i ^ "(/" ^ str ^ ")" ^ "\n"
56 | xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) =
57 indent i ^ "(" ^ str ^ " " ^ flag ^ "=" ^ value ^ ")" ^ "\n" ^
58 List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
59 indent i ^ "(/" ^ str ^ ")" ^ "\n"
60 | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
61 raise ERROR "xmlstr: TODO review attribute \"status\" etc";
63 fun strs2xml strs = foldl (op ^) ("", strs);
65 (*WN071016 checked that _all_ Frontend/interface.sml uses this*)
67 indt (j+i) ^ "<MATHML>\n" ^
68 indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^
69 indt (j+i) ^ "</MATHML>";
70 (*val t = TermC.parse_test @{context} "equality e_";
71 writeln (term2xml 8 t);
73 <ISA> equality e_ </ISA>
76 XML.Elem (("MATHML", []),
77 [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])])
78 fun xml_of_terms ts = map xml_of_term ts
80 (* intermediate replacements while introducing transfer of terms by libisabelle *)
81 fun xml_of_term_NEW (t : term) =
82 XML.Elem (("FORMULA", []), [
83 XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)]),
84 XML.Text ("(TERM)\n " ^ UnparseC.term t ^ "\n(/TERM)")
87 (*version for TextIO*)
88 fun terms2xml _ [] = ""
89 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
90 (*version for writeln: extra \n*)
91 fun terms2xml' _ [] = ""
92 | terms2xml' j [t] = term2xml j t
93 | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;
95 (*WN060513 'cterm' means the Isabelle-type*)
97 indt (j+i) ^ "<MATHML>\n" ^
98 indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^
99 indt (j+i) ^ "</MATHML>\n";
100 fun xml_of_cterm ct =
101 XML.Elem (("MATHML", []),
102 [XML.Elem (("ISA", []), [XML.Text ct])])
104 (*version for TextIO*)
105 fun cterms2xml _ [] = ""
106 | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;
107 (*version for writeln: extra \n*)
108 fun cterms2xml' _ [] = ""
109 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;