# HG changeset patch
# User aspinall
# Date 1183737172 -7200
# Node ID 5ade06703b0775f1b08a878442dae9cf5456c610
# Parent  451ab1a20ac35c7bcf1966de0f54f133606b95ee
Produce good PGML 2.0

diff -r 451ab1a20ac3 -r 5ade06703b07 src/Pure/ProofGeneral/ROOT.ML
--- a/src/Pure/ProofGeneral/ROOT.ML	Fri Jul 06 17:21:18 2007 +0200
+++ b/src/Pure/ProofGeneral/ROOT.ML	Fri Jul 06 17:52:52 2007 +0200
@@ -6,14 +6,14 @@
 *)
 
 use "pgip_types.ML";
+use "pgml.ML";
 use "pgip_markup.ML";
 use "pgip_input.ML";
 use "pgip_output.ML";
 use "pgip.ML";
-use "pgml.ML";
 
 use "pgip_isabelle.ML";
-(*use "pgml_isabelle.ML";*)
+use "pgml_isabelle.ML";
 use "preferences.ML";
 use "parsing.ML";
 
diff -r 451ab1a20ac3 -r 5ade06703b07 src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Fri Jul 06 17:21:18 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Fri Jul 06 17:52:52 2007 +0200
@@ -21,7 +21,7 @@
     | Informfileloaded    of { url: PgipTypes.pgipurl, completed: bool }
     | Informfileoutdated  of { url: PgipTypes.pgipurl, completed: bool }
     | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
-    | Proofstate          of { pgml: XML.content }
+    | Proofstate          of { pgml: Pgml.pgmldoc }
     | Metainforesponse    of { attrs: XML.attributes, 
                                content: XML.content }
     | Lexicalstructure    of { content: XML.content }
@@ -81,7 +81,7 @@
        | Informfileloaded    of { url: Path.T, completed: bool }
        | Informfileoutdated  of { url: Path.T, completed: bool }
        | Informfileretracted of { url: Path.T, completed: bool }
-       | Proofstate          of { pgml: XML.content }
+       | Proofstate          of { pgml: Pgml.pgmldoc }
        | Metainforesponse    of { attrs: XML.attributes, content: XML.content }
        | Lexicalstructure    of { content: XML.content }
        | Proverinfo          of { name: string, version: string, instance: string,
@@ -194,7 +194,7 @@
     let
         val pgml = #pgml vs
     in
-        XML.Elem("proofstate", [], pgml)
+        XML.Elem("proofstate", [], [Pgml.pgmldoc_to_xml pgml])
     end
 
 fun metainforesponse (Metainforesponse vs) =
diff -r 451ab1a20ac3 -r 5ade06703b07 src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Fri Jul 06 17:21:18 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Fri Jul 06 17:52:52 2007 +0200
@@ -101,8 +101,10 @@
       | pgmlaction_to_string Button = "button"
       | pgmlaction_to_string Menu = "menu"
 
-    fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Text content])
-      | atom_to_xml (Str str) = XML.Text str
+    (* 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 pgmlterm_to_xml (Atoms {kind, content}) = 
 	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
diff -r 451ab1a20ac3 -r 5ade06703b07 src/Pure/ProofGeneral/pgml_isabelle.ML
--- a/src/Pure/ProofGeneral/pgml_isabelle.ML	Fri Jul 06 17:21:18 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml_isabelle.ML	Fri Jul 06 17:52:52 2007 +0200
@@ -7,19 +7,22 @@
 
 signature PGML_ISABELLE =
 sig
-    val pgml_of_prettyT : PrettyExt.prettyT -> Pgml.pgmlterm
+(*    val pgml_of_prettyT : Pretty.T -> Pgml.pgmlterm *)
 end
 
 structure PgmlIsabelle : PGML_ISABELLE =
 struct
    open Pgml;
-   open PrettyExt;
+   open Pretty;
 
-   fun pgml_of_prettyT (Block(ts,ind,length)) =
-       Box {orient = SOME HVOrient, indent = SOME ind, content = map pgml_of_prettyT ts}
+(*   fun pgml_of_prettyT1 (Block(ts,ind,length)) =
+       Box {orient = SOME HVOrient, indent = SOME ind, content = map pgml_of_prettyT1 ts}
 
-     | pgml_of_prettyT (String (str,len)) = Atoms { kind = NONE, content = [Str str] }  
+     | pgml_of_prettyT1 (String (str,len)) = Atoms { kind = NONE, content = [Str str] }  
 					    (* TODO: should unquote symbols *)
 
-     | pgml_of_prettyT (Break (flag,ind)) = Pgml.Break { mandatory = SOME flag, indent = SOME ind }
+     | pgml_of_prettyT1 (Break (flag,ind)) = Pgml.Break { mandatory = SOME flag, indent = SOME ind }
+
+   val pgml_of_prettyT = pgml_of_prettyT1 o dest_prettyT;
+*)
 end
diff -r 451ab1a20ac3 -r 5ade06703b07 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 06 17:21:18 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 06 17:52:52 2007 +0200
@@ -244,11 +244,20 @@
 
 fun statedisplay prts =
     let
-        val display = Pretty.output (Pretty.chunks prts)
-        (* TODO: add extra PGML markup for allow proof state navigation *)
-        val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
+        val display = Pretty.chunks prts
+	val pgml = Pgml.Pgml 
+   { version=SOME PgipIsabelle.isabelle_pgml_version_supported, 
+     systemid=SOME PgipIsabelle.systemid,
+     content = Pgml.Subterm 
+		   { kind=SOME "statedisplay",
+		     param=NONE,place=NONE,name=NONE,decoration=NONE,
+		     action=NONE,pos=NONE,xref=NONE,
+		     content=[Pgml.Atoms { kind = NONE,
+					  content = [Pgml.Str  (Pretty.output display)] }] }
+			     (* [PgmlIsabelle.pgml_of_prettyT display] *) }
+ 	            (* TODO: PGML markup for proof state navigation *)
     in
-        issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
+        issue_pgip (Proofstate {pgml=pgml})
     end
 
 fun print_current_goals n m st =