author | Walther Neuper <neuper@ist.tugraz.at> |
Wed, 25 Aug 2010 16:20:07 +0200 | |
branch | isac-update-Isa09-2 |
changeset 37947 | 22235e4dbe5f |
parent 37906 | e2b23ba9df13 |
child 38015 | 67ba02dffacc |
permissions | -rw-r--r-- |
neuper@37906 | 1 |
(* translate formulae from Isabelle-string format to xml-format. |
neuper@37906 | 2 |
TODO implement MathML |
neuper@37906 | 3 |
author: Walther Neuper 030701 |
neuper@37906 | 4 |
(c) isac-team 2003 |
neuper@37906 | 5 |
|
neuper@37906 | 6 |
use"xmlsrc/mathml.sml"; |
neuper@37906 | 7 |
use"mathml.sml"; |
neuper@37906 | 8 |
*) |
neuper@37906 | 9 |
|
neuper@37906 | 10 |
(*.decode Isabelle-strings to the format as seen by the user (1) |
neuper@37906 | 11 |
EXCEPT xml-coding issues (2). |
neuper@37906 | 12 |
(2) have a _reverse_ method |
neuper@37906 | 13 |
'isac.util.parser.FormalizationDigest.decodeEntities' |
neuper@37906 | 14 |
called within Formula#toSMLString in java |
neuper@37906 | 15 |
|
neuper@37947 | 16 |
ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy; |
neuper@37906 | 17 |
ad(2) decode "<" ---> "<", decode ">" ---> ">" |
neuper@37906 | 18 |
decode "&" ---> "&" |
neuper@37947 | 19 |
called for term2xml; + see "fun encode" in Frontend/interface.sml.*) |
neuper@37906 | 20 |
fun decode (str:cterm') = |
neuper@37906 | 21 |
let fun dec [] = [] |
neuper@37906 | 22 |
| dec ("^"::"^"::"^"::cs) = "^"::(dec cs) |
neuper@37906 | 23 |
| dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs) |
neuper@37906 | 24 |
| dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs) |
neuper@37906 | 25 |
| dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs) |
neuper@37906 | 26 |
| dec (c::cs) = c::(dec cs) |
neuper@37906 | 27 |
in (implode o dec o explode) str:cterm' end; |
neuper@37906 | 28 |
|
neuper@37906 | 29 |
|
neuper@37906 | 30 |
fun strs2xml strs = foldl (op ^) ("", strs); |
neuper@37906 | 31 |
(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]); |
neuper@37906 | 32 |
<XXX> xxx </XXX> |
neuper@37906 | 33 |
<YYY> yyy </YYY>*) |
neuper@37906 | 34 |
|
neuper@37906 | 35 |
val indentation = 2; |
neuper@37906 | 36 |
val i = indentation; |
neuper@37906 | 37 |
|
neuper@37947 | 38 |
(*WN071016 checked that _all_ Frontend/interface.sml uses this*) |
neuper@37906 | 39 |
fun term2xml j t = |
neuper@37906 | 40 |
indt (j+i) ^ "<MATHML>\n" ^ |
neuper@37906 | 41 |
indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^ |
neuper@37906 | 42 |
indt (j+i) ^ "</MATHML>"; |
neuper@37906 | 43 |
(*val t = str2term "equality e_"; |
neuper@37906 | 44 |
writeln (term2xml 8 t); |
neuper@37906 | 45 |
<MATHML> |
neuper@37906 | 46 |
<ISA> equality e_ </ISA> |
neuper@37906 | 47 |
<MATHML> *) |
neuper@37906 | 48 |
|
neuper@37906 | 49 |
(*version for TextIO*) |
neuper@37906 | 50 |
fun terms2xml j [] = "" |
neuper@37906 | 51 |
| terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts; |
neuper@37906 | 52 |
(*version for writeln: extra \n*) |
neuper@37906 | 53 |
fun terms2xml' j [] = "" |
neuper@37906 | 54 |
| terms2xml' j [t] = term2xml j t |
neuper@37906 | 55 |
| terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts; |
neuper@37906 | 56 |
|
neuper@37906 | 57 |
(*WN060513 'cterm' means the Isabelle-type*) |
neuper@37906 | 58 |
fun cterm2xml j ct = |
neuper@37906 | 59 |
indt (j+i) ^ "<MATHML>\n" ^ |
neuper@37906 | 60 |
indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^ |
neuper@37906 | 61 |
indt (j+i) ^ "</MATHML>\n"; |
neuper@37906 | 62 |
(*version for TextIO*) |
neuper@37906 | 63 |
fun cterms2xml j [] = "" |
neuper@37906 | 64 |
| cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts; |
neuper@37906 | 65 |
(*version for writeln: extra \n*) |
neuper@37906 | 66 |
fun cterms2xml' j [] = "" |
neuper@37906 | 67 |
| cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts; |
neuper@37906 | 68 |
|
neuper@37906 | 69 |
(* writeln(cterms2xml 5 ["cterm1", "cterm2"]); |
neuper@37906 | 70 |
<MATHML> |
neuper@37906 | 71 |
<ISA> cterm1 </ISA> |
neuper@37906 | 72 |
</MATHML> |
neuper@37906 | 73 |
<MATHML> |
neuper@37906 | 74 |
<ISA> cterm2 </ISA> |
neuper@37906 | 75 |
</MATHML> |
neuper@37906 | 76 |
*) |