# HG changeset patch
# User wenzelm
# Date 1219876399 -7200
# Node ID 7a47b1a8790ec624cec65bbddee523f4ce050fb7
# Parent  915b9a777441d9e9b3fc0667b16f77ecd73484b8
exported atom_to_xml;

diff -r 915b9a777441 -r 7a47b1a8790e src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Thu Aug 28 00:33:17 2008 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Thu Aug 28 00:33:19 2008 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     David Aspinall
 
-PGIP abstraction: PGML 
+PGIP abstraction: PGML
 *)
 
 signature PGML =
@@ -13,13 +13,13 @@
 
     datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
 
-    datatype pgmlplace = Subscript | Superscript | Above | Below 
+    datatype pgmlplace = Subscript | Superscript | Above | Below
 
     datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
 
     datatype pgmlaction = Toggle | Button | Menu
-                                            
-    datatype pgmlterm = 
+
+    datatype pgmlterm =
              Atoms of { kind: string option, content: pgmlatom list }
            | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
            | Break of { mandatory: bool option, indent: int option }
@@ -36,11 +36,12 @@
            | Embed of XML.tree list
            | Raw of XML.tree
 
-    datatype pgml = 
-             Pgml of { version: string option, systemid: string option, 
-                       area: PgipTypes.displayarea option, 
+    datatype pgml =
+             Pgml of { version: string option, systemid: string option,
+                       area: PgipTypes.displayarea option,
                        content: pgmlterm list }
-                       
+
+    val atom_to_xml : pgmlatom -> XML.tree
     val pgmlterm_to_xml : pgmlterm -> XML.tree
 
     val pgml_to_xml : pgml -> XML.tree
@@ -57,13 +58,13 @@
 
     datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
 
-    datatype pgmlplace = Subscript | Superscript | Above | Below 
+    datatype pgmlplace = Subscript | Superscript | Above | Below
 
     datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
 
     datatype pgmlaction = Toggle | Button | Menu
-                                            
-    datatype pgmlterm = 
+
+    datatype pgmlterm =
              Atoms of { kind: string option, content: pgmlatom list }
            | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
            | Break of { mandatory: bool option, indent: int option }
@@ -80,10 +81,10 @@
            | Embed of XML.tree list
            | Raw of XML.tree
 
-                       
-    datatype pgml = 
-             Pgml of { version: string option, systemid: string option, 
-                       area: PgipTypes.displayarea option, 
+
+    datatype pgml =
+             Pgml of { version: string option, systemid: string option,
+                       area: PgipTypes.displayarea option,
                        content: pgmlterm list }
 
     fun pgmlorient_to_string HOVOrient = "hov"
@@ -107,16 +108,16 @@
       | pgmlaction_to_string Button = "button"
       | pgmlaction_to_string Menu = "menu"
 
-    (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; 
-       would be better not to *)
-    fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
-      | atom_to_xml (Str str) = XML.Output str 
-                                                    
-    fun pgmlterm_to_xml (Atoms {kind, content}) = 
-        XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
+    (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
+       would be better not to *)  (* FIXME !??? *)
+    fun atom_to_xml (Sym {name, content}) = XML.Elem ("sym", attr name name, [XML.Text content])
+      | atom_to_xml (Str content) = XML.Text content;
+
+    fun pgmlterm_to_xml (Atoms {kind, content}) =
+        XML.Elem("atom", opt_attr "kind" kind, map atom_to_xml content)
 
       | pgmlterm_to_xml (Box {orient, indent, content}) =
-        XML.Elem("box", 
+        XML.Elem("box",
                  opt_attr_map pgmlorient_to_string "orient" orient @
                  opt_attr_map int_to_pgstring "indent" indent,
                  map pgmlterm_to_xml content)
@@ -127,18 +128,18 @@
                  opt_attr_map int_to_pgstring "indent" indent, [])
 
       | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
-        XML.Elem("subterm", 
+        XML.Elem("subterm",
                  opt_attr "kind" kind @
                  opt_attr "param" param @
                  opt_attr_map pgmlplace_to_string "place" place @
-                 opt_attr "name" name @ 
+                 opt_attr "name" name @
                  opt_attr_map pgmldec_to_string "decoration" decoration @
-                 opt_attr_map pgmlaction_to_string "action" action @ 
+                 opt_attr_map pgmlaction_to_string "action" action @
                  opt_attr "pos" pos @
                  opt_attr_map string_of_pgipurl "xref" xref,
                  map pgmlterm_to_xml content)
 
-      | pgmlterm_to_xml (Alt {kind, content}) = 
+      | pgmlterm_to_xml (Alt {kind, content}) =
         XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
 
       | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
@@ -146,14 +147,14 @@
       | pgmlterm_to_xml (Raw xml) = xml
 
 
-    datatype pgml = 
-             Pgml of { version: string option, systemid: string option, 
-                       area: PgipTypes.displayarea option, 
+    datatype pgml =
+             Pgml of { version: string option, systemid: string option,
+                       area: PgipTypes.displayarea option,
                        content: pgmlterm list }
 
-    fun pgml_to_xml (Pgml {version,systemid,area,content}) = 
+    fun pgml_to_xml (Pgml {version,systemid,area,content}) =
         XML.Elem("pgml",
-                 opt_attr "version" version @ 
+                 opt_attr "version" version @
                  opt_attr "systemid" systemid @
                  Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
                  map pgmlterm_to_xml content)