# HG changeset patch
# User aspinall
# Date 1172877369 -3600
# Node ID ec7ecf70695599de3bd017081ff33a5eaf318ccc
# Parent  6c7f9207fa9edd61b0a0ed4cfc23f9baf0d8f69b
Fix idvalue output and PGML print mode raw encode/decode.

diff -r 6c7f9207fa9e -r ec7ecf706955 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 02 15:43:27 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Mar 03 00:16:09 2007 +0100
@@ -54,7 +54,7 @@
     Symbol.Char s => XML.text s
   | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
   | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
-  | Symbol.Raw s => Symbol.decode_raw s);
+  | Symbol.Raw rs => rs);
 
 fun pgml_output str =
   let val syms = Symbol.explode str
@@ -68,7 +68,7 @@
 
 fun setup_pgml_output () =
   Output.add_mode pgmlN
-    (pgml_output, K pgml_output, Symbol.default_indent, I); (* Symbol.encode_raw); *)
+    (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
 
 end;
 
@@ -703,17 +703,19 @@
 				  text=[XML.Elem("pgmltext",[],
 						 map XML.Rawtext strings)] })
 
-	fun string_of_thm th = Pretty.string_of
+	fun string_of_thm th = Output.output
+			       (Pretty.string_of
 				   (Display.pretty_thm_aux
 					(Sign.pp (Thm.theory_of_thm th))
 					false (* quote *)
 					false (* show hyps *)
 					[] (* asms *)
-					th)
+					th))
 
         fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
 
-	val string_of_thy = Pretty.string_of o (ProofDisplay.pretty_full_theory false)
+	val string_of_thy = Output.output o
+				Pretty.string_of o (ProofDisplay.pretty_full_theory false)
     in
         case (thyname, objtype) of
             (_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]