Revert body of pgml to match schema for now [change bad for Broker]
authoraspinall
Thu, 05 Jul 2007 19:59:01 +0200
changeset 23589 aaba731fce86
parent 23588 4fc6df2c7098
child 23590 ad95084a5c63
Revert body of pgml to match schema for now [change bad for Broker]
src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Thu Jul 05 19:57:19 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Thu Jul 05 19:59:01 2007 +0200
@@ -37,7 +37,7 @@
 
     datatype pgmldoc =
 	     Pgml of { version: string option, systemid: string option, 
-		       content: pgmlterm list }
+		       content: pgmlterm }
 
     val pgmlterm_to_xml : pgmlterm -> XML.tree
 
@@ -78,7 +78,7 @@
 
     datatype pgmldoc =
 	     Pgml of { version: string option, systemid: string option, 
-		       content: pgmlterm list }
+		       content: pgmlterm }
 
     fun pgmlorient_to_string HOVOrient = "hov"
       | pgmlorient_to_string HOrient = "h"
@@ -138,5 +138,5 @@
 
     fun pgmldoc_to_xml (Pgml {version,systemid,content}) = 
 	XML.Elem("pgml",opt_attr "version" version  @ opt_attr "systemid" systemid,
-		 map pgmlterm_to_xml content)
+		 [pgmlterm_to_xml content])
 end