# HG changeset patch
# User wenzelm
# Date 1542033415 -3600
# Node ID fb77612d11ebd278af2244820498d6708f807690
# Parent  bf6937af7fe80a3d2b41689ef7620cf17436166c
tuned signature;

diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/Completion.hs
--- a/src/Tools/Haskell/Completion.hs	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/Completion.hs	Mon Nov 12 15:36:55 2018 +0100
@@ -53,10 +53,7 @@
 markup_report :: [T] -> String
 markup_report [] = ""
 markup_report elems =
-  elems
-  |> map (markup_element #> uncurry XML.Elem)
-  |> XML.Elem Markup.report
-  |> YXML.string_of
+  YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
 
 make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
 make_report limit name_props make_names =
diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Mon Nov 12 15:36:55 2018 +0100
@@ -594,10 +594,7 @@
 markup_report :: [T] -> String
 markup_report [] = ""
 markup_report elems =
-  elems
-  |> map (markup_element #> uncurry XML.Elem)
-  |> XML.Elem Markup.report
-  |> YXML.string_of
+  YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
 
 make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
 make_report limit name_props make_names =
@@ -664,16 +661,16 @@
 
 type Attributes = Properties.T
 type Body = [Tree]
-data Tree = Elem Markup.T Body | Text String
+data Tree = Elem (Markup.T, Body) | Text String
 
 
 {- wrapped elements -}
 
 wrap_elem (((a, atts), body1), body2) =
-  Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)
+  Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)
 
 unwrap_elem
-  (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
+  (Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)) =
   Just (((a, atts), body1), body2)
 unwrap_elem _ = Nothing
 
@@ -685,7 +682,7 @@
     Just (_, ts) -> fold add_content ts
     Nothing ->
       case tree of
-        Elem _ ts -> fold add_content ts
+        Elem (_, ts) -> fold add_content ts
         Text s -> Buffer.add s
 
 content_of body = Buffer.empty |> fold add_content body |> Buffer.content
@@ -704,9 +701,9 @@
   show tree =
     Buffer.empty |> show_tree tree |> Buffer.content
     where
-      show_tree (Elem (name, atts) []) =
+      show_tree (Elem ((name, atts), [])) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
-      show_tree (Elem (name, atts) ts) =
+      show_tree (Elem ((name, atts), ts)) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
         fold show_tree ts #>
         Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
@@ -763,11 +760,11 @@
 
 -- structural nodes
 
-node = XML.Elem (":", [])
+node ts = XML.Elem ((":", []), ts)
 
 vector = map_index (\(i, x) -> (int_atom i, x))
 
-tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
+tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
 
 
 -- representation of standard types
@@ -776,7 +773,7 @@
 tree t = [t]
 
 properties :: T Properties.T
-properties props = [XML.Elem (":", props) []]
+properties props = [XML.Elem ((":", props), [])]
 
 string :: T String
 string "" = []
@@ -859,13 +856,13 @@
 
 {- structural nodes -}
 
-node (XML.Elem (":", []) ts) = ts
+node (XML.Elem ((":", []), ts)) = ts
 node _ = err_body
 
 vector atts =
   map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
 
-tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
+tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
 tagged _ = err_body
 
 
@@ -876,7 +873,7 @@
 tree _ = err_body
 
 properties :: T Properties.T
-properties [XML.Elem (":", props) []] = props
+properties [XML.Elem ((":", props), [])] = props
 properties _ = err_body
 
 string :: T String
@@ -969,7 +966,7 @@
 buffer_body = fold buffer
 
 buffer :: XML.Tree -> Buffer.T -> Buffer.T
-buffer (XML.Elem (name, atts) ts) =
+buffer (XML.Elem ((name, atts), ts)) =
   Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   buffer_body ts #>
   Buffer.add strXYX
@@ -1014,7 +1011,7 @@
 push name atts pending = ((name, atts), []) : pending
 
 pop ((("", _), _) : _) = err_unbalanced ""
-pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
+pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
 
 
 -- parsing
@@ -1084,7 +1081,7 @@
 
 symbolic_markup markup body =
   if Markup.is_empty markup then body
-  else [XML.Elem markup body]
+  else [XML.Elem (markup, body)]
 
 symbolic :: T -> XML.Body
 symbolic (Block markup consistent indent prts) =
@@ -1092,7 +1089,7 @@
   |> symbolic_markup block_markup
   |> symbolic_markup markup
   where block_markup = if null prts then Markup.empty else Markup.block consistent indent
-symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
+symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
 symbolic (Str s) = symbolic_text s
 
 formatted :: T -> String
diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/Pretty.hs
--- a/src/Tools/Haskell/Pretty.hs	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/Pretty.hs	Mon Nov 12 15:36:55 2018 +0100
@@ -40,7 +40,7 @@
 
 symbolic_markup markup body =
   if Markup.is_empty markup then body
-  else [XML.Elem markup body]
+  else [XML.Elem (markup, body)]
 
 symbolic :: T -> XML.Body
 symbolic (Block markup consistent indent prts) =
@@ -48,7 +48,7 @@
   |> symbolic_markup block_markup
   |> symbolic_markup markup
   where block_markup = if null prts then Markup.empty else Markup.block consistent indent
-symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
+symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
 symbolic (Str s) = symbolic_text s
 
 formatted :: T -> String
diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/XML.hs
--- a/src/Tools/Haskell/XML.hs	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/XML.hs	Mon Nov 12 15:36:55 2018 +0100
@@ -24,16 +24,16 @@
 
 type Attributes = Properties.T
 type Body = [Tree]
-data Tree = Elem Markup.T Body | Text String
+data Tree = Elem (Markup.T, Body) | Text String
 
 
 {- wrapped elements -}
 
 wrap_elem (((a, atts), body1), body2) =
-  Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)
+  Elem (("xml_elem", ("xml_name", a) : atts), Elem (("xml_body", []), body1) : body2)
 
 unwrap_elem
-  (Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)) =
+  (Elem (("xml_elem", ("xml_name", a) : atts), Elem (("xml_body", []), body1) : body2)) =
   Just (((a, atts), body1), body2)
 unwrap_elem _ = Nothing
 
@@ -45,7 +45,7 @@
     Just (_, ts) -> fold add_content ts
     Nothing ->
       case tree of
-        Elem _ ts -> fold add_content ts
+        Elem (_, ts) -> fold add_content ts
         Text s -> Buffer.add s
 
 content_of body = Buffer.empty |> fold add_content body |> Buffer.content
@@ -64,9 +64,9 @@
   show tree =
     Buffer.empty |> show_tree tree |> Buffer.content
     where
-      show_tree (Elem (name, atts) []) =
+      show_tree (Elem ((name, atts), [])) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
-      show_tree (Elem (name, atts) ts) =
+      show_tree (Elem ((name, atts), ts)) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
         fold show_tree ts #>
         Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/XML/Decode.hs
--- a/src/Tools/Haskell/XML/Decode.hs	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/XML/Decode.hs	Mon Nov 12 15:36:55 2018 +0100
@@ -54,13 +54,13 @@
 
 {- structural nodes -}
 
-node (XML.Elem (":", []) ts) = ts
+node (XML.Elem ((":", []), ts)) = ts
 node _ = err_body
 
 vector atts =
   map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
 
-tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
+tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
 tagged _ = err_body
 
 
@@ -71,7 +71,7 @@
 tree _ = err_body
 
 properties :: T Properties.T
-properties [XML.Elem (":", props) []] = props
+properties [XML.Elem ((":", props), [])] = props
 properties _ = err_body
 
 string :: T String
diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/XML/Encode.hs
--- a/src/Tools/Haskell/XML/Encode.hs	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/XML/Encode.hs	Mon Nov 12 15:36:55 2018 +0100
@@ -44,11 +44,11 @@
 
 -- structural nodes
 
-node = XML.Elem (":", [])
+node ts = XML.Elem ((":", []), ts)
 
 vector = map_index (\(i, x) -> (int_atom i, x))
 
-tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
+tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
 
 
 -- representation of standard types
@@ -57,7 +57,7 @@
 tree t = [t]
 
 properties :: T Properties.T
-properties props = [XML.Elem (":", props) []]
+properties props = [XML.Elem ((":", props), [])]
 
 string :: T String
 string "" = []
diff -r bf6937af7fe8 -r fb77612d11eb src/Tools/Haskell/YXML.hs
--- a/src/Tools/Haskell/YXML.hs	Mon Nov 12 15:14:12 2018 +0100
+++ b/src/Tools/Haskell/YXML.hs	Mon Nov 12 15:36:55 2018 +0100
@@ -53,7 +53,7 @@
 buffer_body = fold buffer
 
 buffer :: XML.Tree -> Buffer.T -> Buffer.T
-buffer (XML.Elem (name, atts) ts) =
+buffer (XML.Elem ((name, atts), ts)) =
   Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   buffer_body ts #>
   Buffer.add strXYX
@@ -98,7 +98,7 @@
 push name atts pending = ((name, atts), []) : pending
 
 pop ((("", _), _) : _) = err_unbalanced ""
-pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
+pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
 
 
 -- parsing