handle output of Text nodes when writing XML trees
git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@3173 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
parent
190a9166dd
commit
a8f529d490
|
@ -273,7 +273,10 @@ fun writeIndent stream 0 = ()
|
||||||
| writeIndent stream n = (TextIO.output (stream, " "); writeIndent stream (n-1))
|
| writeIndent stream n = (TextIO.output (stream, " "); writeIndent stream (n-1))
|
||||||
|
|
||||||
|
|
||||||
fun writeXmlTree indent stream tree =
|
fun writeXmlTree indent stream (Text s) =
|
||||||
|
(writeIndent stream indent;
|
||||||
|
TextIO.output (stream, s^"\n"))
|
||||||
|
| writeXmlTree indent stream tree =
|
||||||
let val elemName = escape (tagname_of tree)
|
let val elemName = escape (tagname_of tree)
|
||||||
in
|
in
|
||||||
writeIndent stream indent;
|
writeIndent stream indent;
|
||||||
|
|
Loading…
Reference in New Issue