src/Pure/ProofGeneral/pgml.ML
changeset 23610 5ade06703b07
parent 23589 aaba731fce86
child 23723 4fff46d5faaa
equal deleted inserted replaced
23609:451ab1a20ac3 23610:5ade06703b07
    99 
    99 
   100     fun pgmlaction_to_string Toggle = "toggle"
   100     fun pgmlaction_to_string Toggle = "toggle"
   101       | pgmlaction_to_string Button = "button"
   101       | pgmlaction_to_string Button = "button"
   102       | pgmlaction_to_string Menu = "menu"
   102       | pgmlaction_to_string Menu = "menu"
   103 
   103 
   104     fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Text content])
   104     (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; 
   105       | atom_to_xml (Str str) = XML.Text str
   105        would be better not to *)
       
   106     fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Rawtext content])
       
   107       | atom_to_xml (Str str) = XML.Rawtext str 
   106 						    
   108 						    
   107     fun pgmlterm_to_xml (Atoms {kind, content}) = 
   109     fun pgmlterm_to_xml (Atoms {kind, content}) = 
   108 	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
   110 	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
   109 
   111 
   110       | pgmlterm_to_xml (Box {orient, indent, content}) =
   112       | pgmlterm_to_xml (Box {orient, indent, content}) =