# HG changeset patch # User aspinall # Date 1183576823 -7200 # Node ID 0cd175710a9328ca20e8f11ec079384ac41c5edf # Parent 37532c9df22c1fd634a9de98fd35f9344bacb3c9 PGML abstraction, draft version diff -r 37532c9df22c -r 0cd175710a93 src/Pure/ProofGeneral/pgml.ML --- /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 diff -r 37532c9df22c -r 0cd175710a93 src/Pure/ProofGeneral/pgml_isabelle.ML --- /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