src/Tools/Haskell/Haskell.thy

   encode = encode . Text.pack
   decode :: Bytes -> String
   decode = Text.unpack . decode
 \<close>
 
-generate_file "Isabelle/Symbol.hs" = \<open>
-{-  Title:      Isabelle/Symbols.hs
-    Author:     Makarius
-    LICENSE:    BSD 3-clause (Isabelle)
-
-Isabelle text symbols.
--}
-
-module Isabelle.Symbol where
-
-{- ASCII characters -}
-
-is_ascii_letter :: Char -> Bool
-is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
-
-is_ascii_digit :: Char -> Bool
-is_ascii_digit c = '0' <= c && c <= '9'
-
-is_ascii_hex :: Char -> Bool
-is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
-
-is_ascii_quasi :: Char -> Bool
-is_ascii_quasi c = c == '_' || c == '\''
-
-is_ascii_blank :: Char -> Bool
-is_ascii_blank c = c `elem` " \t\n\11\f\r"
-
-is_ascii_line_terminator :: Char -> Bool
-is_ascii_line_terminator c = c == '\r' || c == '\n'
-
-is_ascii_letdig :: Char -> Bool
-is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
-
-is_ascii_identifier :: String -> Bool
-is_ascii_identifier s =
-  not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
-\<close>
-
 generate_file "Isabelle/Library.hs" = \<open>
 {-  Title:      Isabelle/Library.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 

       _ -> line
   else line
 
 clean_name :: String -> String
 clean_name = reverse #> dropWhile (== '_') #> reverse
+\<close>
+
+
+generate_file "Isabelle/Symbol.hs" = \<open>
+{-  Title:      Isabelle/Symbols.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Isabelle text symbols.
+-}
+
+module Isabelle.Symbol where
+
+{- ASCII characters -}
+
+is_ascii_letter :: Char -> Bool
+is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
+
+is_ascii_digit :: Char -> Bool
+is_ascii_digit c = '0' <= c && c <= '9'
+
+is_ascii_hex :: Char -> Bool
+is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
+
+is_ascii_quasi :: Char -> Bool
+is_ascii_quasi c = c == '_' || c == '\''
+
+is_ascii_blank :: Char -> Bool
+is_ascii_blank c = c `elem` " \t\n\11\f\r"
+
+is_ascii_line_terminator :: Char -> Bool
+is_ascii_line_terminator c = c == '\r' || c == '\n'
+
+is_ascii_letdig :: Char -> Bool
+is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
+
+is_ascii_identifier :: String -> Bool
+is_ascii_identifier s =
+  not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
 \<close>
 
 generate_file "Isabelle/Value.hs" = \<open>
 {-  Title:      Isabelle/Value.hs
     Author:     Makarius

 
 no_output :: Output
 no_output = ("", "")
 \<close>
 
+generate_file "Isabelle/XML.hs" = \<open>
+{-  Title:      Isabelle/XML.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Untyped XML trees and representation of ML values.
+
+See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+-}
+
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
+module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
+where
+
+import Isabelle.Library
+import qualified Isabelle.Properties as Properties
+import qualified Isabelle.Markup as Markup
+import qualified Isabelle.Buffer as Buffer
+
+
+{- types -}
+
+type Attributes = Properties.T
+type Body = [Tree]
+data Tree = Elem (Markup.T, Body) | Text String
+
+
+{- wrapped elements -}
+
+wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
+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)
+
+unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
+unwrap_elem
+  (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
+
+
+{- text content -}
+
+add_content :: Tree -> Buffer.T -> Buffer.T
+add_content tree =
+  case unwrap_elem tree of
+    Just (_, ts) -> fold add_content ts
+    Nothing ->
+      case tree of
+        Elem (_, ts) -> fold add_content ts
+        Text s -> Buffer.add s
+
+content_of :: Body -> String
+content_of body = Buffer.empty |> fold add_content body |> Buffer.content
+
+
+{- string representation -}
+
+encode '<' = "&lt;"
+encode '>' = "&gt;"
+encode '&' = "&amp;"
+encode '\'' = "&apos;"
+encode '\"' = "&quot;"
+encode c = [c]
+
+instance Show Tree where
+  show tree =
+    Buffer.empty |> show_tree tree |> Buffer.content
+    where
+      show_tree (Elem ((name, atts), [])) =
+        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
+      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 ">"
+      show_tree (Text s) = Buffer.add (show_text s)
+
+      show_elem name atts =
+        unwords (name : map (\(a, x) -> a <> "=\"" <> show_text x <> "\"") atts)
+
+      show_text = concatMap encode
+\<close>
+
+generate_file "Isabelle/XML/Encode.hs" = \<open>
+{-  Title:      Isabelle/XML/Encode.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+XML as data representation language.
+
+See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+-}
+
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
+module Isabelle.XML.Encode (
+  A, T, V, P,
+
+  int_atom, bool_atom, unit_atom,
+
+  tree, properties, string, int, bool, unit, pair, triple, list, option, variant
+)
+where
+
+import Isabelle.Library
+import qualified Isabelle.Value as Value
+import qualified Isabelle.Properties as Properties
+import qualified Isabelle.XML as XML
+
+
+type A a = a -> String
+type T a = a -> XML.Body
+type V a = a -> Maybe ([String], XML.Body)
+type P a = a -> [String]
+
+
+-- atomic values
+
+int_atom :: A Int
+int_atom = Value.print_int
+
+bool_atom :: A Bool
+bool_atom False = "0"
+bool_atom True = "1"
+
+unit_atom :: A ()
+unit_atom () = ""
+
+
+-- structural nodes
+
+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)
+
+
+-- representation of standard types
+
+tree :: T XML.Tree
+tree t = [t]
+
+properties :: T Properties.T
+properties props = [XML.Elem ((":", props), [])]
+
+string :: T String
+string "" = []
+string s = [XML.Text s]
+
+int :: T Int
+int = string . int_atom
+
+bool :: T Bool
+bool = string . bool_atom
+
+unit :: T ()
+unit = string . unit_atom
+
+pair :: T a -> T b -> T (a, b)
+pair f g (x, y) = [node (f x), node (g y)]
+
+triple :: T a -> T b -> T c -> T (a, b, c)
+triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
+
+list :: T a -> T [a]
+list f xs = map (node . f) xs
+
+option :: T a -> T (Maybe a)
+option _ Nothing = []
+option f (Just x) = [node (f x)]
+
+variant :: [V a] -> T a
+variant fs x = [tagged (the (get_index (\f -> f x) fs))]
+\<close>
+
+generate_file "Isabelle/XML/Decode.hs" = \<open>
+{-  Title:      Isabelle/XML/Decode.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+XML as data representation language.
+
+See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+-}
+
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
+module Isabelle.XML.Decode (
+  A, T, V, P,
+
+  int_atom, bool_atom, unit_atom,
+
+  tree, properties, string, int, bool, unit, pair, triple, list, option, variant
+)
+where
+
+import Isabelle.Library
+import qualified Isabelle.Value as Value
+import qualified Isabelle.Properties as Properties
+import qualified Isabelle.XML as XML
+
+
+type A a = String -> a
+type T a = XML.Body -> a
+type V a = ([String], XML.Body) -> a
+type P a = [String] -> a
+
+err_atom = error "Malformed XML atom"
+err_body = error "Malformed XML body"
+
+
+{- atomic values -}
+
+int_atom :: A Int
+int_atom s =
+  case Value.parse_int s of
+    Just i -> i
+    Nothing -> err_atom
+
+bool_atom :: A Bool
+bool_atom "0" = False
+bool_atom "1" = True
+bool_atom _ = err_atom
+
+unit_atom :: A ()
+unit_atom "" = ()
+unit_atom _ = err_atom
+
+
+{- structural nodes -}
+
+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 _ = err_body
+
+
+{- representation of standard types -}
+
+tree :: T XML.Tree
+tree [t] = t
+tree _ = err_body
+
+properties :: T Properties.T
+properties [XML.Elem ((":", props), [])] = props
+properties _ = err_body
+
+string :: T String
+string [] = ""
+string [XML.Text s] = s
+string _ = err_body
+
+int :: T Int
+int = int_atom . string
+
+bool :: T Bool
+bool = bool_atom . string
+
+unit :: T ()
+unit = unit_atom . string
+
+pair :: T a -> T b -> T (a, b)
+pair f g [t1, t2] = (f (node t1), g (node t2))
+pair _ _ _ = err_body
+
+triple :: T a -> T b -> T c -> T (a, b, c)
+triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
+triple _ _ _ _ = err_body
+
+list :: T a -> T [a]
+list f ts = map (f . node) ts
+
+option :: T a -> T (Maybe a)
+option _ [] = Nothing
+option f [t] = Just (f (node t))
+option _ _ = err_body
+
+variant :: [V a] -> T a
+variant fs [t] = (fs !! tag) (xs, ts)
+  where (tag, (xs, ts)) = tagged t
+variant _ _ = err_body
+\<close>
+
+generate_file "Isabelle/YXML.hs" = \<open>
+{-  Title:      Isabelle/YXML.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Efficient text representation of XML trees.  Suitable for direct
+inlining into plain text.
+
+See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
+-}
+
+{-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-}
+
+module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
+  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
+where
+
+import qualified Data.Char as Char
+import qualified Data.List as List
+
+import Isabelle.Library
+import qualified Isabelle.Markup as Markup
+import qualified Isabelle.XML as XML
+import qualified Isabelle.Buffer as Buffer
+
+
+{- markers -}
+
+charX, charY :: Char
+charX = Char.chr 5
+charY = Char.chr 6
+
+strX, strY, strXY, strXYX :: String
+strX = [charX]
+strY = [charY]
+strXY = strX <> strY
+strXYX = strXY <> strX
+
+detect :: String -> Bool
+detect = any (\c -> c == charX || c == charY)
+
+
+{- output -}
+
+output_markup :: Markup.T -> Markup.Output
+output_markup markup@(name, atts) =
+  if Markup.is_empty markup then Markup.no_output
+  else (strXY <> name <> concatMap (\(a, x) -> strY <> a <> "=" <> x) atts <> strX, strXYX)
+
+buffer_attrib (a, x) =
+  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
+
+buffer_body :: XML.Body -> Buffer.T -> Buffer.T
+buffer_body = fold buffer
+
+buffer :: XML.Tree -> Buffer.T -> Buffer.T
+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
+buffer (XML.Text s) = Buffer.add s
+
+string_of_body :: XML.Body -> String
+string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
+
+string_of :: XML.Tree -> String
+string_of = string_of_body . single
+
+
+{- parse -}
+
+-- split: fields or non-empty tokens
+
+split :: Bool -> Char -> String -> [String]
+split _ _ [] = []
+split fields sep str = splitting str
+  where
+    splitting rest =
+      case span (/= sep) rest of
+        (_, []) -> cons rest []
+        (prfx, _ : rest') -> cons prfx (splitting rest')
+    cons item = if fields || not (null item) then (:) item else id
+
+
+-- structural errors
+
+err msg = error ("Malformed YXML: " <> msg)
+err_attribute = err "bad attribute"
+err_element = err "bad element"
+err_unbalanced "" = err "unbalanced element"
+err_unbalanced name = err ("unbalanced element " <> quote name)
+
+
+-- stack operations
+
+add x ((elem, body) : pending) = (elem, x : body) : pending
+
+push "" _ _ = err_element
+push name atts pending = ((name, atts), []) : pending
+
+pop ((("", _), _) : _) = err_unbalanced ""
+pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
+
+
+-- parsing
+
+parse_attrib s =
+  case List.elemIndex '=' s of
+    Just i | i > 0 -> (take i s, drop (i + 1) s)
+    _ -> err_attribute
+
+parse_chunk ["", ""] = pop
+parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
+parse_chunk txts = fold (add . XML.Text) txts
+
+parse_body :: String -> XML.Body
+parse_body source =
+  case fold parse_chunk chunks [(("", []), [])] of
+    [(("", _), result)] -> reverse result
+    ((name, _), _) : _ -> err_unbalanced name
+  where chunks = split False charX source |> map (split True charY)
+
+parse :: String -> XML.Tree
+parse source =
+  case parse_body source of
+    [result] -> result
+    [] -> XML.Text ""
+    _ -> err "multiple results"
+\<close>
+
 generate_file "Isabelle/Completion.hs" = \<open>
 {-  Title:      Isabelle/Completion.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 

   IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s)
 
 append :: IO.FilePath -> String -> IO ()
 append path s =
   IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
-\<close>
-
-generate_file "Isabelle/XML.hs" = \<open>
-{-  Title:      Isabelle/XML.hs
-    Author:     Makarius
-    LICENSE:    BSD 3-clause (Isabelle)
-
-Untyped XML trees and representation of ML values.
-
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
--}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-
-module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
-where
-
-import Isabelle.Library
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.Buffer as Buffer
-
-
-{- types -}
-
-type Attributes = Properties.T
-type Body = [Tree]
-data Tree = Elem (Markup.T, Body) | Text String
-
-
-{- wrapped elements -}
-
-wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
-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)
-
-unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
-unwrap_elem
-  (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
-
-
-{- text content -}
-
-add_content :: Tree -> Buffer.T -> Buffer.T
-add_content tree =
-  case unwrap_elem tree of
-    Just (_, ts) -> fold add_content ts
-    Nothing ->
-      case tree of
-        Elem (_, ts) -> fold add_content ts
-        Text s -> Buffer.add s
-
-content_of :: Body -> String
-content_of body = Buffer.empty |> fold add_content body |> Buffer.content
-
-
-{- string representation -}
-
-encode '<' = "&lt;"
-encode '>' = "&gt;"
-encode '&' = "&amp;"
-encode '\'' = "&apos;"
-encode '\"' = "&quot;"
-encode c = [c]
-
-instance Show Tree where
-  show tree =
-    Buffer.empty |> show_tree tree |> Buffer.content
-    where
-      show_tree (Elem ((name, atts), [])) =
-        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
-      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 ">"
-      show_tree (Text s) = Buffer.add (show_text s)
-
-      show_elem name atts =
-        unwords (name : map (\(a, x) -> a <> "=\"" <> show_text x <> "\"") atts)
-
-      show_text = concatMap encode
-\<close>
-
-generate_file "Isabelle/XML/Encode.hs" = \<open>
-{-  Title:      Isabelle/XML/Encode.hs
-    Author:     Makarius
-    LICENSE:    BSD 3-clause (Isabelle)
-
-XML as data representation language.
-
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
--}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-
-module Isabelle.XML.Encode (
-  A, T, V, P,
-
-  int_atom, bool_atom, unit_atom,
-
-  tree, properties, string, int, bool, unit, pair, triple, list, option, variant
-)
-where
-
-import Isabelle.Library
-import qualified Isabelle.Value as Value
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.XML as XML
-
-
-type A a = a -> String
-type T a = a -> XML.Body
-type V a = a -> Maybe ([String], XML.Body)
-type P a = a -> [String]
-
-
--- atomic values
-
-int_atom :: A Int
-int_atom = Value.print_int
-
-bool_atom :: A Bool
-bool_atom False = "0"
-bool_atom True = "1"
-
-unit_atom :: A ()
-unit_atom () = ""
-
-
--- structural nodes
-
-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)
-
-
--- representation of standard types
-
-tree :: T XML.Tree
-tree t = [t]
-
-properties :: T Properties.T
-properties props = [XML.Elem ((":", props), [])]
-
-string :: T String
-string "" = []
-string s = [XML.Text s]
-
-int :: T Int
-int = string . int_atom
-
-bool :: T Bool
-bool = string . bool_atom
-
-unit :: T ()
-unit = string . unit_atom
-
-pair :: T a -> T b -> T (a, b)
-pair f g (x, y) = [node (f x), node (g y)]
-
-triple :: T a -> T b -> T c -> T (a, b, c)
-triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
-
-list :: T a -> T [a]
-list f xs = map (node . f) xs
-
-option :: T a -> T (Maybe a)
-option _ Nothing = []
-option f (Just x) = [node (f x)]
-
-variant :: [V a] -> T a
-variant fs x = [tagged (the (get_index (\f -> f x) fs))]
-\<close>
-
-generate_file "Isabelle/XML/Decode.hs" = \<open>
-{-  Title:      Isabelle/XML/Decode.hs
-    Author:     Makarius
-    LICENSE:    BSD 3-clause (Isabelle)
-
-XML as data representation language.
-
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
--}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-
-module Isabelle.XML.Decode (
-  A, T, V, P,
-
-  int_atom, bool_atom, unit_atom,
-
-  tree, properties, string, int, bool, unit, pair, triple, list, option, variant
-)
-where
-
-import Isabelle.Library
-import qualified Isabelle.Value as Value
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.XML as XML
-
-
-type A a = String -> a
-type T a = XML.Body -> a
-type V a = ([String], XML.Body) -> a
-type P a = [String] -> a
-
-err_atom = error "Malformed XML atom"
-err_body = error "Malformed XML body"
-
-
-{- atomic values -}
-
-int_atom :: A Int
-int_atom s =
-  case Value.parse_int s of
-    Just i -> i
-    Nothing -> err_atom
-
-bool_atom :: A Bool
-bool_atom "0" = False
-bool_atom "1" = True
-bool_atom _ = err_atom
-
-unit_atom :: A ()
-unit_atom "" = ()
-unit_atom _ = err_atom
-
-
-{- structural nodes -}
-
-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 _ = err_body
-
-
-{- representation of standard types -}
-
-tree :: T XML.Tree
-tree [t] = t
-tree _ = err_body
-
-properties :: T Properties.T
-properties [XML.Elem ((":", props), [])] = props
-properties _ = err_body
-
-string :: T String
-string [] = ""
-string [XML.Text s] = s
-string _ = err_body
-
-int :: T Int
-int = int_atom . string
-
-bool :: T Bool
-bool = bool_atom . string
-
-unit :: T ()
-unit = unit_atom . string
-
-pair :: T a -> T b -> T (a, b)
-pair f g [t1, t2] = (f (node t1), g (node t2))
-pair _ _ _ = err_body
-
-triple :: T a -> T b -> T c -> T (a, b, c)
-triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
-triple _ _ _ _ = err_body
-
-list :: T a -> T [a]
-list f ts = map (f . node) ts
-
-option :: T a -> T (Maybe a)
-option _ [] = Nothing
-option f [t] = Just (f (node t))
-option _ _ = err_body
-
-variant :: [V a] -> T a
-variant fs [t] = (fs !! tag) (xs, ts)
-  where (tag, (xs, ts)) = tagged t
-variant _ _ = err_body
-\<close>
-
-generate_file "Isabelle/YXML.hs" = \<open>
-{-  Title:      Isabelle/YXML.hs
-    Author:     Makarius
-    LICENSE:    BSD 3-clause (Isabelle)
-
-Efficient text representation of XML trees.  Suitable for direct
-inlining into plain text.
-
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
--}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-}
-
-module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
-  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
-where
-
-import qualified Data.Char as Char
-import qualified Data.List as List
-
-import Isabelle.Library
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.XML as XML
-import qualified Isabelle.Buffer as Buffer
-
-
-{- markers -}
-
-charX, charY :: Char
-charX = Char.chr 5
-charY = Char.chr 6
-
-strX, strY, strXY, strXYX :: String
-strX = [charX]
-strY = [charY]
-strXY = strX <> strY
-strXYX = strXY <> strX
-
-detect :: String -> Bool
-detect = any (\c -> c == charX || c == charY)
-
-
-{- output -}
-
-output_markup :: Markup.T -> Markup.Output
-output_markup markup@(name, atts) =
-  if Markup.is_empty markup then Markup.no_output
-  else (strXY <> name <> concatMap (\(a, x) -> strY <> a <> "=" <> x) atts <> strX, strXYX)
-
-buffer_attrib (a, x) =
-  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
-
-buffer_body :: XML.Body -> Buffer.T -> Buffer.T
-buffer_body = fold buffer
-
-buffer :: XML.Tree -> Buffer.T -> Buffer.T
-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
-buffer (XML.Text s) = Buffer.add s
-
-string_of_body :: XML.Body -> String
-string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
-
-string_of :: XML.Tree -> String
-string_of = string_of_body . single
-
-
-{- parse -}
-
--- split: fields or non-empty tokens
-
-split :: Bool -> Char -> String -> [String]
-split _ _ [] = []
-split fields sep str = splitting str
-  where
-    splitting rest =
-      case span (/= sep) rest of
-        (_, []) -> cons rest []
-        (prfx, _ : rest') -> cons prfx (splitting rest')
-    cons item = if fields || not (null item) then (:) item else id
-
-
--- structural errors
-
-err msg = error ("Malformed YXML: " <> msg)
-err_attribute = err "bad attribute"
-err_element = err "bad element"
-err_unbalanced "" = err "unbalanced element"
-err_unbalanced name = err ("unbalanced element " <> quote name)
-
-
--- stack operations
-
-add x ((elem, body) : pending) = (elem, x : body) : pending
-
-push "" _ _ = err_element
-push name atts pending = ((name, atts), []) : pending
-
-pop ((("", _), _) : _) = err_unbalanced ""
-pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
-
-
--- parsing
-
-parse_attrib s =
-  case List.elemIndex '=' s of
-    Just i | i > 0 -> (take i s, drop (i + 1) s)
-    _ -> err_attribute
-
-parse_chunk ["", ""] = pop
-parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
-parse_chunk txts = fold (add . XML.Text) txts
-
-parse_body :: String -> XML.Body
-parse_body source =
-  case fold parse_chunk chunks [(("", []), [])] of
-    [(("", _), result)] -> reverse result
-    ((name, _), _) : _ -> err_unbalanced name
-  where chunks = split False charX source |> map (split True charY)
-
-parse :: String -> XML.Tree
-parse source =
-  case parse_body source of
-    [result] -> result
-    [] -> XML.Text ""
-    _ -> err "multiple results"
 \<close>
 
 generate_file "Isabelle/Pretty.hs" = \<open>
 {-  Title:      Isabelle/Pretty.hs
     Author:     Makarius