<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
No, there's no standard support now for serialization to XML.<br>
<br>
<div class="moz-cite-prefix">On 04/14/2014 10:21 AM, Marco Maggesi
wrote:<br>
</div>
<blockquote
cite="mid:CAAdZW_vAfOw9C6vCeEnfFpuO_2SorJrN5hRHr_5KNDF+_6TgtQ@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">
Ah, good.</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">Thanks,
This solves my problem.<br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">As
a side curiosity, can the serialised type family be used to
encode/decode to xml?<br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">
<br>
</div>
</div>
<div class="gmail_extra"><br>
<br>
<div class="gmail_quote">2014-04-14 14:16 GMT+02:00 Adam
Chlipala <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:adamc@csail.mit.edu" target="_blank">adamc@csail.mit.edu</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#ffffff" text="#000000">
<div class="">
On 04/14/2014 03:13 AM, Marco Maggesi wrote:
<blockquote type="cite">
<div dir="ltr">I have a tree-like datatype as follows
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">
<div class="gmail_default">datatype tree =</div>
<div class="gmail_default"> | Leaf of { Label :
string }</div>
<div class="gmail_default"> | Node of { Label :
string, Children :
list tree}</div>
<div><br>
</div>
<div>and I would like to write values of tree type
inside an SQL
database.</div>
</div>
</div>
</blockquote>
<br>
</div>
I expect the built-in [serialized] type family is exactly
what you
want. You could help me test the documentation, by seeing
if this tip
is enough to point you in the right direction without more
detail
here. :)<br>
</div>
</blockquote>
</div>
</div>
</blockquote>
</body>
</html>