Produce good PGML 2.0
authoraspinall
Fri Jul 06 17:52:52 2007 +0200 (2007-07-06)
changeset 236105ade06703b07
parent 23609 451ab1a20ac3
child 23611 65b168646309
Produce good PGML 2.0
src/Pure/ProofGeneral/ROOT.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgml.ML
src/Pure/ProofGeneral/pgml_isabelle.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Fri Jul 06 17:21:18 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Fri Jul 06 17:52:52 2007 +0200
     1.3 @@ -6,14 +6,14 @@
     1.4  *)
     1.5  
     1.6  use "pgip_types.ML";
     1.7 +use "pgml.ML";
     1.8  use "pgip_markup.ML";
     1.9  use "pgip_input.ML";
    1.10  use "pgip_output.ML";
    1.11  use "pgip.ML";
    1.12 -use "pgml.ML";
    1.13  
    1.14  use "pgip_isabelle.ML";
    1.15 -(*use "pgml_isabelle.ML";*)
    1.16 +use "pgml_isabelle.ML";
    1.17  use "preferences.ML";
    1.18  use "parsing.ML";
    1.19  
     2.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Fri Jul 06 17:21:18 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Fri Jul 06 17:52:52 2007 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4      | Informfileloaded    of { url: PgipTypes.pgipurl, completed: bool }
     2.5      | Informfileoutdated  of { url: PgipTypes.pgipurl, completed: bool }
     2.6      | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
     2.7 -    | Proofstate          of { pgml: XML.content }
     2.8 +    | Proofstate          of { pgml: Pgml.pgmldoc }
     2.9      | Metainforesponse    of { attrs: XML.attributes, 
    2.10                                 content: XML.content }
    2.11      | Lexicalstructure    of { content: XML.content }
    2.12 @@ -81,7 +81,7 @@
    2.13         | Informfileloaded    of { url: Path.T, completed: bool }
    2.14         | Informfileoutdated  of { url: Path.T, completed: bool }
    2.15         | Informfileretracted of { url: Path.T, completed: bool }
    2.16 -       | Proofstate          of { pgml: XML.content }
    2.17 +       | Proofstate          of { pgml: Pgml.pgmldoc }
    2.18         | Metainforesponse    of { attrs: XML.attributes, content: XML.content }
    2.19         | Lexicalstructure    of { content: XML.content }
    2.20         | Proverinfo          of { name: string, version: string, instance: string,
    2.21 @@ -194,7 +194,7 @@
    2.22      let
    2.23          val pgml = #pgml vs
    2.24      in
    2.25 -        XML.Elem("proofstate", [], pgml)
    2.26 +        XML.Elem("proofstate", [], [Pgml.pgmldoc_to_xml pgml])
    2.27      end
    2.28  
    2.29  fun metainforesponse (Metainforesponse vs) =
     3.1 --- a/src/Pure/ProofGeneral/pgml.ML	Fri Jul 06 17:21:18 2007 +0200
     3.2 +++ b/src/Pure/ProofGeneral/pgml.ML	Fri Jul 06 17:52:52 2007 +0200
     3.3 @@ -101,8 +101,10 @@
     3.4        | pgmlaction_to_string Button = "button"
     3.5        | pgmlaction_to_string Menu = "menu"
     3.6  
     3.7 -    fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Text content])
     3.8 -      | atom_to_xml (Str str) = XML.Text str
     3.9 +    (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; 
    3.10 +       would be better not to *)
    3.11 +    fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Rawtext content])
    3.12 +      | atom_to_xml (Str str) = XML.Rawtext str 
    3.13  						    
    3.14      fun pgmlterm_to_xml (Atoms {kind, content}) = 
    3.15  	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
     4.1 --- a/src/Pure/ProofGeneral/pgml_isabelle.ML	Fri Jul 06 17:21:18 2007 +0200
     4.2 +++ b/src/Pure/ProofGeneral/pgml_isabelle.ML	Fri Jul 06 17:52:52 2007 +0200
     4.3 @@ -7,19 +7,22 @@
     4.4  
     4.5  signature PGML_ISABELLE =
     4.6  sig
     4.7 -    val pgml_of_prettyT : PrettyExt.prettyT -> Pgml.pgmlterm
     4.8 +(*    val pgml_of_prettyT : Pretty.T -> Pgml.pgmlterm *)
     4.9  end
    4.10  
    4.11  structure PgmlIsabelle : PGML_ISABELLE =
    4.12  struct
    4.13     open Pgml;
    4.14 -   open PrettyExt;
    4.15 +   open Pretty;
    4.16  
    4.17 -   fun pgml_of_prettyT (Block(ts,ind,length)) =
    4.18 -       Box {orient = SOME HVOrient, indent = SOME ind, content = map pgml_of_prettyT ts}
    4.19 +(*   fun pgml_of_prettyT1 (Block(ts,ind,length)) =
    4.20 +       Box {orient = SOME HVOrient, indent = SOME ind, content = map pgml_of_prettyT1 ts}
    4.21  
    4.22 -     | pgml_of_prettyT (String (str,len)) = Atoms { kind = NONE, content = [Str str] }  
    4.23 +     | pgml_of_prettyT1 (String (str,len)) = Atoms { kind = NONE, content = [Str str] }  
    4.24  					    (* TODO: should unquote symbols *)
    4.25  
    4.26 -     | pgml_of_prettyT (Break (flag,ind)) = Pgml.Break { mandatory = SOME flag, indent = SOME ind }
    4.27 +     | pgml_of_prettyT1 (Break (flag,ind)) = Pgml.Break { mandatory = SOME flag, indent = SOME ind }
    4.28 +
    4.29 +   val pgml_of_prettyT = pgml_of_prettyT1 o dest_prettyT;
    4.30 +*)
    4.31  end
     5.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 06 17:21:18 2007 +0200
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 06 17:52:52 2007 +0200
     5.3 @@ -244,11 +244,20 @@
     5.4  
     5.5  fun statedisplay prts =
     5.6      let
     5.7 -        val display = Pretty.output (Pretty.chunks prts)
     5.8 -        (* TODO: add extra PGML markup for allow proof state navigation *)
     5.9 -        val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
    5.10 +        val display = Pretty.chunks prts
    5.11 +	val pgml = Pgml.Pgml 
    5.12 +   { version=SOME PgipIsabelle.isabelle_pgml_version_supported, 
    5.13 +     systemid=SOME PgipIsabelle.systemid,
    5.14 +     content = Pgml.Subterm 
    5.15 +		   { kind=SOME "statedisplay",
    5.16 +		     param=NONE,place=NONE,name=NONE,decoration=NONE,
    5.17 +		     action=NONE,pos=NONE,xref=NONE,
    5.18 +		     content=[Pgml.Atoms { kind = NONE,
    5.19 +					  content = [Pgml.Str  (Pretty.output display)] }] }
    5.20 +			     (* [PgmlIsabelle.pgml_of_prettyT display] *) }
    5.21 + 	            (* TODO: PGML markup for proof state navigation *)
    5.22      in
    5.23 -        issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
    5.24 +        issue_pgip (Proofstate {pgml=pgml})
    5.25      end
    5.26  
    5.27  fun print_current_goals n m st =