From a8f529d4904d0378c2a288b119456ac659d6c987 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?J=C3=BCrgen=20Doser?= <doserj@inf.ethz.ch>
Date: Wed, 5 Oct 2005 16:13:27 +0000
Subject: [PATCH] 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
---
 src/xmltree_parser.sml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/xmltree_parser.sml b/src/xmltree_parser.sml
index 1ced0e2..88ae172 100644
--- a/src/xmltree_parser.sml
+++ b/src/xmltree_parser.sml
@@ -273,7 +273,10 @@ fun writeIndent stream 0 = ()
   | 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)
     in 
 	writeIndent stream indent;