--- 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 =
--- 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
--- 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
--- 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 ">"
--- 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
--- 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 "" = []
--- 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