src/Pure/ProofGeneral/pgml.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 26548 41bbcaf3e481
child 28020 1ff5167592ba
permissions -rw-r--r--
map_const: soft version, no failure here;
     1 (*  Title:      Pure/ProofGeneral/pgml.ML
     2     ID:         $Id$
     3     Author:     David Aspinall
     4 
     5 PGIP abstraction: PGML 
     6 *)
     7 
     8 signature PGML =
     9 sig
    10     type pgmlsym = { name: string, content: string }
    11 
    12     datatype pgmlatom = Sym of pgmlsym | Str of string
    13 
    14     datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
    15 
    16     datatype pgmlplace = Subscript | Superscript | Above | Below 
    17 
    18     datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
    19 
    20     datatype pgmlaction = Toggle | Button | Menu
    21 					    
    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
    38 
    39     datatype pgml = 
    40 	     Pgml of { version: string option, systemid: string option, 
    41 		       area: PgipTypes.displayarea option, 
    42 		       content: pgmlterm list }
    43 		       
    44     val pgmlterm_to_xml : pgmlterm -> XML.tree
    45 
    46     val pgml_to_xml : pgml -> XML.tree
    47 end
    48 
    49 
    50 structure Pgml : PGML =
    51 struct
    52     open PgipTypes
    53 
    54     type pgmlsym = { name: string, content: string }
    55 
    56     datatype pgmlatom = Sym of pgmlsym | Str of string
    57 
    58     datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
    59 
    60     datatype pgmlplace = Subscript | Superscript | Above | Below 
    61 
    62     datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
    63 
    64     datatype pgmlaction = Toggle | Button | Menu
    65 					    
    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
    82 
    83 		       
    84     datatype pgml = 
    85 	     Pgml of { version: string option, systemid: string option, 
    86 		       area: PgipTypes.displayarea option, 
    87 		       content: pgmlterm list }
    88 
    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"
    93 
    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"
    98 
    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"
   105 
   106     fun pgmlaction_to_string Toggle = "toggle"
   107       | pgmlaction_to_string Button = "button"
   108       | pgmlaction_to_string Menu = "menu"
   109 
   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 
   114 						    
   115     fun pgmlterm_to_xml (Atoms {kind, content}) = 
   116 	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
   117 
   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)
   123 
   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, [])
   128 
   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)
   140 
   141       | pgmlterm_to_xml (Alt {kind, content}) = 
   142 	XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
   143 
   144       | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
   145 
   146       | pgmlterm_to_xml (Raw xml) = xml
   147 
   148 
   149     datatype pgml = 
   150 	     Pgml of { version: string option, systemid: string option, 
   151 		       area: PgipTypes.displayarea option, 
   152 		       content: pgmlterm list }
   153 
   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