tuned;
authorwenzelm
Mon Nov 05 11:29:11 2018 +0100 (6 months ago)
changeset 69236a75aab6d785b
parent 69235 0e156963b636
child 69237 76696742fd30
tuned;
src/Tools/Haskell/Haskell.thy
src/Tools/Haskell/XML.hs
     1.1 --- a/src/Tools/Haskell/Haskell.thy	Mon Nov 05 10:02:21 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Mon Nov 05 11:29:11 2018 +0100
     1.3 @@ -481,16 +481,12 @@
     1.4  
     1.5  {- wrapped elements -}
     1.6  
     1.7 -xml_elemN = \<open>XML.xml_elemN\<close>
     1.8 -xml_nameN = \<open>XML.xml_nameN\<close>
     1.9 -xml_bodyN = \<open>XML.xml_bodyN\<close>
    1.10 +wrap_elem (((a, atts), body1), body2) =
    1.11 +  Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)
    1.12  
    1.13 -wrap_elem (((a, atts), body1), body2) =
    1.14 -  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
    1.15 -
    1.16 -unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
    1.17 -  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
    1.18 -  then Just (((a, atts), body1), body2) else Nothing
    1.19 +unwrap_elem
    1.20 +  (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
    1.21 +  Just (((a, atts), body1), body2)
    1.22  unwrap_elem _ = Nothing
    1.23  
    1.24  
     2.1 --- a/src/Tools/Haskell/XML.hs	Mon Nov 05 10:02:21 2018 +0100
     2.2 +++ b/src/Tools/Haskell/XML.hs	Mon Nov 05 11:29:11 2018 +0100
     2.3 @@ -27,16 +27,12 @@
     2.4  
     2.5  {- wrapped elements -}
     2.6  
     2.7 -xml_elemN = "xml_elem"
     2.8 -xml_nameN = "xml_name"
     2.9 -xml_bodyN = "xml_body"
    2.10 +wrap_elem (((a, atts), body1), body2) =
    2.11 +  Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)
    2.12  
    2.13 -wrap_elem (((a, atts), body1), body2) =
    2.14 -  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
    2.15 -
    2.16 -unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
    2.17 -  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
    2.18 -  then Just (((a, atts), body1), body2) else Nothing
    2.19 +unwrap_elem
    2.20 +  (Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)) =
    2.21 +  Just (((a, atts), body1), body2)
    2.22  unwrap_elem _ = Nothing
    2.23  
    2.24