# HG changeset patch
# User wenzelm
# Date 1184102989 -7200
# Node ID 4fff46d5faaa2f242e52f3c3bfd957570b451f7c
# Parent  a4af559708abe3fa631c68f6dca35c3775d2c256
renamed XML.Rawtext to XML.Output;

diff -r a4af559708ab -r 4fff46d5faaa src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Tue Jul 10 23:29:47 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Tue Jul 10 23:29:49 2007 +0200
@@ -103,8 +103,8 @@
 
     (* 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.Rawtext content])
-      | atom_to_xml (Str str) = XML.Rawtext str 
+    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)
diff -r a4af559708ab -r 4fff46d5faaa src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 10 23:29:47 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 10 23:29:49 2007 +0200
@@ -147,7 +147,7 @@
   XML.string_of_tree o PgipOutput.output o assemble_pgips o map PgipOutput.output;
 
 fun issue_pgip_rawtext str =
-    output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str]))
+    output_xml (PgipOutput.output (assemble_pgips [XML.Output str]))
 
 fun issue_pgips pgipops =
     output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
@@ -173,7 +173,7 @@
     (* Normal responses are messages for the user *)
     fun normalmsg area cat urgent s =
         let
-            val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
+            val content = XML.Elem("pgmltext",[],[XML.Output s])
             val pgip = Normalresponse {area=area,messagecategory=cat,
                                        urgent=urgent,content=[content] }
         in
@@ -183,7 +183,7 @@
     (* Error responses are error messages for the user, or system-level messages *)
     fun errormsg fatality s =
         let
-              val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
+              val content = XML.Elem("pgmltext",[],[XML.Output s])
               val pgip = Errorresponse {area=NONE,fatality=fatality,
                                         content=[content],
                                         location=NONE}
@@ -194,7 +194,7 @@
     (* Error responses with useful locations *)
     fun error_with_pos fatality pos s =
         let
-              val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
+              val content = XML.Elem("pgmltext",[],[XML.Output s])
               val pgip = Errorresponse {area=NONE,fatality=fatality,
                                         content=[content],
                                         location=SOME (PgipIsabelle.location_of_position pos)}
@@ -716,7 +716,7 @@
         fun idvalue strings =
             issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, 
                                   text=[XML.Elem("pgmltext",[],
-                                                 map XML.Rawtext strings)] })
+                                                 map XML.Output strings)] })
 
         fun string_of_thm th = Output.output
                                (Pretty.string_of
@@ -997,7 +997,7 @@
                               (XML.string_of_tree xml))
            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
       | XML.Text t => ignored_text_warning t
-      | XML.Rawtext t => ignored_text_warning t
+      | XML.Output t => ignored_text_warning t
 and ignored_text_warning t =
     if size (Symbol.strip_blanks t) > 0 then
            warning ("Ignored text in PGIP packet: \n" ^ t)
diff -r a4af559708ab -r 4fff46d5faaa src/Pure/Tools/xml.ML
--- a/src/Pure/Tools/xml.ML	Tue Jul 10 23:29:47 2007 +0200
+++ b/src/Pure/Tools/xml.ML	Tue Jul 10 23:29:49 2007 +0200
@@ -18,8 +18,8 @@
   (* tree functions *)
   datatype tree =
       Elem of string * attributes * tree list
-    | Text of string    (*native string, subject to XML.text on output*)
-    | Rawtext of string (*XML string: output directly, not parsed*)
+    | Text of string
+    | Output of output
   type content = tree list
   type element = string * attributes * content
   val string_of_tree: tree -> string
@@ -84,7 +84,7 @@
 datatype tree =
     Elem of string * attributes * tree list
   | Text of string
-  | Rawtext of string;
+  | Output of output;
 
 type content = tree list;
 
@@ -105,7 +105,7 @@
             |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
         end
       | string_of (Text s) buf = Buffer.add (text s) buf
-      | string_of (Rawtext s) buf = Buffer.add s buf;
+      | string_of (Output s) buf = Buffer.add s buf;
   in string_of tree Buffer.empty end;
 
 val string_of_tree = Buffer.content o buffer_of_tree;