PGML abstraction, draft version

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgml.ML	Wed Jul 04 21:20:23 2007 +0200
@@ -0,0 +1,142 @@
+(*  Title:      Pure/ProofGeneral/pgip_types.ML
+    ID:         $Id$
+    Author:     David Aspinall
+
+PGIP abstraction: PGML 
+*)
+
+signature PGML =
+sig
+    type pgmlsym = { name: string, content: string }
+
+    datatype pgmlatom = Sym of pgmlsym | Str of string
+
+    datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
+
+    datatype pgmlplace = Subscript | Superscript | Above | Below 
+
+    datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
+
+    datatype pgmlaction = Toggle | Button | Menu
+					    
+    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 }
+	   | Subterm of { kind: string option,
+			  param: string option,
+			  place: pgmlplace option,
+			  name: string option,
+			  decoration: pgmldec option,
+			  action: pgmlaction option,
+			  pos: string option,
+			  xref: PgipTypes.pgipurl option,
+			  content: pgmlterm list }
+	   | Alt of { kind: string option, content: pgmlterm list }
+	   | Embed of XML.tree list
+
+    datatype pgmldoc =
+	     Pgml of { version: string option, systemid: string option, 
+		       content: pgmlterm list }
+
+    val pgmlterm_to_xml : pgmlterm -> XML.tree
+
+    val pgmldoc_to_xml : pgmldoc -> XML.tree
+end
+
+
+structure Pgml : PGML =
+struct
+    open PgipTypes
+
+    type pgmlsym = { name: string, content: string }
+    datatype pgmlatom = Sym of pgmlsym | Str of string
+
+    datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
+
+    datatype pgmlplace = Subscript | Superscript | Above | Below 
+
+    datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
+
+    datatype pgmlaction = Toggle | Button | Menu
+					    
+    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 }
+	   | Subterm of { kind: string option,
+			  param: string option,
+			  place: pgmlplace option,
+			  name: string option,
+			  decoration: pgmldec option,
+			  action: pgmlaction option,
+			  pos: string option,
+			  xref: PgipTypes.pgipurl option,
+			  content: pgmlterm list }
+	   | Alt of { kind: string option, content: pgmlterm list }
+	   | Embed of XML.tree list
+
+    datatype pgmldoc =
+	     Pgml of { version: string option, systemid: string option, 
+		       content: pgmlterm list }
+
+    fun pgmlorient_to_string HOVOrient = "hov"
+      | pgmlorient_to_string HOrient = "h"
+      | pgmlorient_to_string VOrient = "v"
+      | pgmlorient_to_string HVOrient = "hv"
+
+    fun pgmlplace_to_string Subscript = "sub"
+      | pgmlplace_to_string Superscript = "sup"
+      | pgmlplace_to_string Above = "above"
+      | pgmlplace_to_string Below = "below"
+
+    fun pgmldec_to_string Bold = "bold"
+      | pgmldec_to_string Italic = "italic"
+      | pgmldec_to_string Error = "error"
+      | pgmldec_to_string Warning = "warning"
+      | pgmldec_to_string Info = "info"
+      | pgmldec_to_string (Other s) = "other"
+
+    fun pgmlaction_to_string Toggle = "toggle"
+      | 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
+						    
+    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", 
+		 opt_attr_map pgmlorient_to_string "orient" orient @
+		 opt_attr_map int_to_pgstring "indent" indent,
+		 map pgmlterm_to_xml content)
+
+      | pgmlterm_to_xml (Break {mandatory, indent}) =
+	XML.Elem("break",
+		 opt_attr_map bool_to_pgstring "mandatory" mandatory @
+		 opt_attr_map int_to_pgstring "indent" indent, [])
+
+      | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
+	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_map pgmldec_to_string "decoration" decoration @
+		 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}) = 
+	XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
+
+      | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
+
+
+    fun pgmldoc_to_xml (Pgml {version,systemid,content}) = 
+	XML.Elem("pgml",opt_attr "version" version  @ opt_attr "systemid" systemid,
+		 map pgmlterm_to_xml content)
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgml_isabelle.ML	Wed Jul 04 21:20:23 2007 +0200
@@ -0,0 +1,25 @@
+(*  Title:      Pure/ProofGeneral/pgip_types.ML
+    ID:         $Id$
+    Author:     David Aspinall
+
+PGIP abstraction: marshalling between PGML and Isabelle types
+*)
+
+signature PGML_ISABELLE =
+sig
+    val pgml_of_prettyT : PrettyExt.prettyT -> Pgml.pgmlterm
+end
+
+structure PgmlIsabelle : PGML_ISABELLE =
+struct
+   open Pgml;
+   open PrettyExt;
+
+   fun pgml_of_prettyT (Block(ts,ind,length)) =
+       Box {orient = SOME HVOrient, indent = SOME ind, content = map pgml_of_prettyT ts}
+
+     | pgml_of_prettyT (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 }
+end