src/Pure/ProofGeneral/pgml.ML

filtering out some package theorems

(*  Title:      Pure/ProofGeneral/pgml.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.content
	   | Raw of XML.tree

    datatype pgml = 
	     Pgml of { version: string option, systemid: string option, 
		       area: PgipTypes.displayarea option, 
		       content: pgmlterm list }
		       
    val pgmlterm_to_xml : pgmlterm -> XML.tree

    val pgml_to_xml : pgml -> 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.content
	   | Raw of XML.tree

		       
    datatype pgml = 
	     Pgml of { version: string option, systemid: string option, 
		       area: PgipTypes.displayarea 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"

    (* 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.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)

      | 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)

      | pgmlterm_to_xml (Raw xml) = xml


    datatype pgml = 
	     Pgml of { version: string option, systemid: string option, 
		       area: PgipTypes.displayarea option, 
		       content: pgmlterm list }

    fun pgml_to_xml (Pgml {version,systemid,area,content}) = 
	XML.Elem("pgml",
		 opt_attr "version" version @ 
		 opt_attr "systemid" systemid @
		 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
		 map pgmlterm_to_xml content)
end