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;
haftmann@24584
     1
(*  Title:      Pure/ProofGeneral/pgml.ML
aspinall@23571
     2
    ID:         $Id$
aspinall@23571
     3
    Author:     David Aspinall
aspinall@23571
     4
aspinall@23571
     5
PGIP abstraction: PGML 
aspinall@23571
     6
*)
aspinall@23571
     7
aspinall@23571
     8
signature PGML =
aspinall@23571
     9
sig
aspinall@23571
    10
    type pgmlsym = { name: string, content: string }
aspinall@23571
    11
aspinall@23571
    12
    datatype pgmlatom = Sym of pgmlsym | Str of string
aspinall@23571
    13
aspinall@23571
    14
    datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
aspinall@23571
    15
aspinall@23571
    16
    datatype pgmlplace = Subscript | Superscript | Above | Below 
aspinall@23571
    17
aspinall@23571
    18
    datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
aspinall@23571
    19
aspinall@23571
    20
    datatype pgmlaction = Toggle | Button | Menu
aspinall@23571
    21
					    
aspinall@23571
    22
    datatype pgmlterm = 
aspinall@23571
    23
	     Atoms of { kind: string option, content: pgmlatom list }
aspinall@23571
    24
	   | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
aspinall@23571
    25
	   | Break of { mandatory: bool option, indent: int option }
aspinall@23571
    26
	   | Subterm of { kind: string option,
aspinall@23571
    27
			  param: string option,
aspinall@23571
    28
			  place: pgmlplace option,
aspinall@23571
    29
			  name: string option,
aspinall@23571
    30
			  decoration: pgmldec option,
aspinall@23571
    31
			  action: pgmlaction option,
aspinall@23571
    32
			  pos: string option,
aspinall@23571
    33
			  xref: PgipTypes.pgipurl option,
aspinall@23571
    34
			  content: pgmlterm list }
aspinall@23571
    35
	   | Alt of { kind: string option, content: pgmlterm list }
wenzelm@26548
    36
	   | Embed of XML.tree list
aspinall@23748
    37
	   | Raw of XML.tree
aspinall@23571
    38
aspinall@23748
    39
    datatype pgml = 
aspinall@23571
    40
	     Pgml of { version: string option, systemid: string option, 
aspinall@23748
    41
		       area: PgipTypes.displayarea option, 
aspinall@23748
    42
		       content: pgmlterm list }
aspinall@23748
    43
		       
aspinall@23571
    44
    val pgmlterm_to_xml : pgmlterm -> XML.tree
aspinall@23571
    45
aspinall@23748
    46
    val pgml_to_xml : pgml -> XML.tree
aspinall@23571
    47
end
aspinall@23571
    48
aspinall@23571
    49
aspinall@23571
    50
structure Pgml : PGML =
aspinall@23571
    51
struct
aspinall@23571
    52
    open PgipTypes
aspinall@23571
    53
aspinall@23571
    54
    type pgmlsym = { name: string, content: string }
aspinall@23748
    55
aspinall@23571
    56
    datatype pgmlatom = Sym of pgmlsym | Str of string
aspinall@23571
    57
aspinall@23571
    58
    datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
aspinall@23571
    59
aspinall@23571
    60
    datatype pgmlplace = Subscript | Superscript | Above | Below 
aspinall@23571
    61
aspinall@23571
    62
    datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
aspinall@23571
    63
aspinall@23571
    64
    datatype pgmlaction = Toggle | Button | Menu
aspinall@23571
    65
					    
aspinall@23571
    66
    datatype pgmlterm = 
aspinall@23571
    67
	     Atoms of { kind: string option, content: pgmlatom list }
aspinall@23571
    68
	   | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
aspinall@23571
    69
	   | Break of { mandatory: bool option, indent: int option }
aspinall@23571
    70
	   | Subterm of { kind: string option,
aspinall@23571
    71
			  param: string option,
aspinall@23571
    72
			  place: pgmlplace option,
aspinall@23571
    73
			  name: string option,
aspinall@23571
    74
			  decoration: pgmldec option,
aspinall@23571
    75
			  action: pgmlaction option,
aspinall@23571
    76
			  pos: string option,
aspinall@23571
    77
			  xref: PgipTypes.pgipurl option,
aspinall@23571
    78
			  content: pgmlterm list }
aspinall@23571
    79
	   | Alt of { kind: string option, content: pgmlterm list }
wenzelm@26548
    80
	   | Embed of XML.tree list
aspinall@23748
    81
	   | Raw of XML.tree
aspinall@23571
    82
aspinall@23748
    83
		       
aspinall@23748
    84
    datatype pgml = 
aspinall@23571
    85
	     Pgml of { version: string option, systemid: string option, 
aspinall@23748
    86
		       area: PgipTypes.displayarea option, 
aspinall@23748
    87
		       content: pgmlterm list }
aspinall@23571
    88
aspinall@23571
    89
    fun pgmlorient_to_string HOVOrient = "hov"
aspinall@23571
    90
      | pgmlorient_to_string HOrient = "h"
aspinall@23571
    91
      | pgmlorient_to_string VOrient = "v"
aspinall@23571
    92
      | pgmlorient_to_string HVOrient = "hv"
aspinall@23571
    93
aspinall@23571
    94
    fun pgmlplace_to_string Subscript = "sub"
aspinall@23571
    95
      | pgmlplace_to_string Superscript = "sup"
aspinall@23571
    96
      | pgmlplace_to_string Above = "above"
aspinall@23571
    97
      | pgmlplace_to_string Below = "below"
aspinall@23571
    98
aspinall@23571
    99
    fun pgmldec_to_string Bold = "bold"
aspinall@23571
   100
      | pgmldec_to_string Italic = "italic"
aspinall@23571
   101
      | pgmldec_to_string Error = "error"
aspinall@23571
   102
      | pgmldec_to_string Warning = "warning"
aspinall@23571
   103
      | pgmldec_to_string Info = "info"
aspinall@23571
   104
      | pgmldec_to_string (Other s) = "other"
aspinall@23571
   105
aspinall@23571
   106
    fun pgmlaction_to_string Toggle = "toggle"
aspinall@23571
   107
      | pgmlaction_to_string Button = "button"
aspinall@23571
   108
      | pgmlaction_to_string Menu = "menu"
aspinall@23571
   109
aspinall@23610
   110
    (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; 
aspinall@23610
   111
       would be better not to *)
wenzelm@23723
   112
    fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
wenzelm@23723
   113
      | atom_to_xml (Str str) = XML.Output str 
aspinall@23571
   114
						    
aspinall@23571
   115
    fun pgmlterm_to_xml (Atoms {kind, content}) = 
aspinall@23571
   116
	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
aspinall@23571
   117
aspinall@23571
   118
      | pgmlterm_to_xml (Box {orient, indent, content}) =
aspinall@23571
   119
	XML.Elem("box", 
aspinall@23571
   120
		 opt_attr_map pgmlorient_to_string "orient" orient @
aspinall@23571
   121
		 opt_attr_map int_to_pgstring "indent" indent,
aspinall@23571
   122
		 map pgmlterm_to_xml content)
aspinall@23571
   123
aspinall@23571
   124
      | pgmlterm_to_xml (Break {mandatory, indent}) =
aspinall@23571
   125
	XML.Elem("break",
aspinall@23571
   126
		 opt_attr_map bool_to_pgstring "mandatory" mandatory @
aspinall@23571
   127
		 opt_attr_map int_to_pgstring "indent" indent, [])
aspinall@23571
   128
aspinall@23571
   129
      | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
aspinall@23571
   130
	XML.Elem("subterm", 
aspinall@23571
   131
  		 opt_attr "kind" kind @
aspinall@23571
   132
		 opt_attr "param" param @
aspinall@23571
   133
		 opt_attr_map pgmlplace_to_string "place" place @
aspinall@23571
   134
		 opt_attr "name" name @ 
aspinall@23571
   135
		 opt_attr_map pgmldec_to_string "decoration" decoration @
aspinall@23571
   136
		 opt_attr_map pgmlaction_to_string "action" action @ 
aspinall@23571
   137
		 opt_attr "pos" pos @
aspinall@23571
   138
		 opt_attr_map string_of_pgipurl "xref" xref,
aspinall@23571
   139
		 map pgmlterm_to_xml content)
aspinall@23571
   140
aspinall@23571
   141
      | pgmlterm_to_xml (Alt {kind, content}) = 
aspinall@23571
   142
	XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
aspinall@23571
   143
aspinall@23571
   144
      | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
aspinall@23571
   145
aspinall@23748
   146
      | pgmlterm_to_xml (Raw xml) = xml
aspinall@23571
   147
aspinall@23748
   148
aspinall@23748
   149
    datatype pgml = 
aspinall@23748
   150
	     Pgml of { version: string option, systemid: string option, 
aspinall@23748
   151
		       area: PgipTypes.displayarea option, 
aspinall@23748
   152
		       content: pgmlterm list }
aspinall@23748
   153
aspinall@23748
   154
    fun pgml_to_xml (Pgml {version,systemid,area,content}) = 
aspinall@23748
   155
	XML.Elem("pgml",
aspinall@23748
   156
		 opt_attr "version" version @ 
aspinall@23748
   157
		 opt_attr "systemid" systemid @
aspinall@23748
   158
		 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
aspinall@23748
   159
		 map pgmlterm_to_xml content)
aspinall@23571
   160
end