wneuper/isa: src/Pure/ProofGeneral/pgml.ML@1ff5167592ba

     1 (*  Title:      Pure/ProofGeneral/pgml.ML

     2     ID:         $Id$

     3     Author:     David Aspinall

     5 PGIP abstraction: PGML

     6 *)

     8 signature PGML =

     9 sig

    10     type pgmlsym = { name: string, content: string }

    12     datatype pgmlatom = Sym of pgmlsym | Str of string

    14     datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient

    16     datatype pgmlplace = Subscript | Superscript | Above | Below

    18     datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string

    20     datatype pgmlaction = Toggle | Button | Menu

    22     datatype pgmlterm =

    23              Atoms of { kind: string option, content: pgmlatom list }

    24            | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }

    25            | Break of { mandatory: bool option, indent: int option }

    26            | Subterm of { kind: string option,

    27                           param: string option,

    28                           place: pgmlplace option,

    29                           name: string option,

    30                           decoration: pgmldec option,

    31                           action: pgmlaction option,

    32                           pos: string option,

    33                           xref: PgipTypes.pgipurl option,

    34                           content: pgmlterm list }

    35            | Alt of { kind: string option, content: pgmlterm list }

    36            | Embed of XML.tree list

    37            | Raw of XML.tree

    39     datatype pgml =

    40              Pgml of { version: string option, systemid: string option,

    41                        area: PgipTypes.displayarea option,

    42                        content: pgmlterm list }

    44     val pgmlterm_to_xml : pgmlterm -> XML.tree

    46     val pgml_to_xml : pgml -> XML.tree

    47 end

    50 structure Pgml : PGML =

    51 struct

    52     open PgipTypes

    54     type pgmlsym = { name: string, content: string }

    56     datatype pgmlatom = Sym of pgmlsym | Str of string

    58     datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient

    60     datatype pgmlplace = Subscript | Superscript | Above | Below

    62     datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string

    64     datatype pgmlaction = Toggle | Button | Menu

    66     datatype pgmlterm =

    67              Atoms of { kind: string option, content: pgmlatom list }

    68            | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }

    69            | Break of { mandatory: bool option, indent: int option }

    70            | Subterm of { kind: string option,

    71                           param: string option,

    72                           place: pgmlplace option,

    73                           name: string option,

    74                           decoration: pgmldec option,

    75                           action: pgmlaction option,

    76                           pos: string option,

    77                           xref: PgipTypes.pgipurl option,

    78                           content: pgmlterm list }

    79            | Alt of { kind: string option, content: pgmlterm list }

    80            | Embed of XML.tree list

    81            | Raw of XML.tree

    84     datatype pgml =

    85              Pgml of { version: string option, systemid: string option,

    86                        area: PgipTypes.displayarea option,

    87                        content: pgmlterm list }

    89     fun pgmlorient_to_string HOVOrient = "hov"

    90       | pgmlorient_to_string HOrient = "h"

    91       | pgmlorient_to_string VOrient = "v"

    92       | pgmlorient_to_string HVOrient = "hv"

    94     fun pgmlplace_to_string Subscript = "sub"

    95       | pgmlplace_to_string Superscript = "sup"

    96       | pgmlplace_to_string Above = "above"

    97       | pgmlplace_to_string Below = "below"

    99     fun pgmldec_to_string Bold = "bold"

   100       | pgmldec_to_string Italic = "italic"

   101       | pgmldec_to_string Error = "error"

   102       | pgmldec_to_string Warning = "warning"

   103       | pgmldec_to_string Info = "info"

   104       | pgmldec_to_string (Other s) = "other"

   106     fun pgmlaction_to_string Toggle = "toggle"

   107       | pgmlaction_to_string Button = "button"

   108       | pgmlaction_to_string Menu = "menu"

   110     (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;

   111        would be better not to *)

   112     fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])

   113       | atom_to_xml (Str str) = XML.Output str

   115     fun pgmlterm_to_xml (Atoms {kind, content}) =

   116         XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)

   118       | pgmlterm_to_xml (Box {orient, indent, content}) =

   119         XML.Elem("box",

   120                  opt_attr_map pgmlorient_to_string "orient" orient @

   121                  opt_attr_map int_to_pgstring "indent" indent,

   122                  map pgmlterm_to_xml content)

   124       | pgmlterm_to_xml (Break {mandatory, indent}) =

   125         XML.Elem("break",

   126                  opt_attr_map bool_to_pgstring "mandatory" mandatory @

   127                  opt_attr_map int_to_pgstring "indent" indent, [])

   129       | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =

   130         XML.Elem("subterm",

   131                  opt_attr "kind" kind @

   132                  opt_attr "param" param @

   133                  opt_attr_map pgmlplace_to_string "place" place @

   134                  opt_attr "name" name @

   135                  opt_attr_map pgmldec_to_string "decoration" decoration @

   136                  opt_attr_map pgmlaction_to_string "action" action @

   137                  opt_attr "pos" pos @

   138                  opt_attr_map string_of_pgipurl "xref" xref,

   139                  map pgmlterm_to_xml content)

   141       | pgmlterm_to_xml (Alt {kind, content}) =

   142         XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)

   144       | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)

   146       | pgmlterm_to_xml (Raw xml) = xml

   149     datatype pgml =

   150              Pgml of { version: string option, systemid: string option,

   151                        area: PgipTypes.displayarea option,

   152                        content: pgmlterm list }

   154     fun pgml_to_xml (Pgml {version,systemid,area,content}) =

   155         XML.Elem("pgml",

   156                  opt_attr "version" version @

   157                  opt_attr "systemid" systemid @

   158                  Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),

   159                  map pgmlterm_to_xml content)

   160 end

author	wenzelm
	Wed, 27 Aug 2008 12:00:28 +0200
changeset 28020	1ff5167592ba
parent 26548	41bbcaf3e481
child 28038	7a47b1a8790e
permissions	-rw-r--r--