src/Tools/Haskell/Haskell.thy

 
   the, the_default,
 
   fold, fold_rev, single, map_index, get_index,
 
-  quote, trim_line, clean_name)
+  quote, space_implode, commas, commas_quote, cat_lines,
+  space_explode, split_lines, trim_line, clean_name)
 where
 
 import Data.Maybe
+import qualified Data.List as List
+import qualified Data.List.Split as Split
 
 
 {- functions -}
 
 (|>) :: a -> (a -> b) -> b

 
 {- strings -}
 
 quote :: String -> String
 quote s = "\"" ++ s ++ "\""
+
+space_implode :: String -> [String] -> String
+space_implode = List.intercalate
+
+commas, commas_quote :: [String] -> String
+commas = space_implode ", "
+commas_quote = commas . map quote
+
+cat_lines :: [String] -> String
+cat_lines = space_implode "\n"
+
+
+space_explode :: Char -> String -> [String]
+space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
+
+split_lines :: String -> [String]
+split_lines = space_explode '\n'
 
 trim_line :: String -> String
 trim_line line =
   case reverse line of
     '\n' : '\r' : rest -> reverse rest

   str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
   item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
   commas, enclose, enum, list, str_list, big_list)
 where
 
-import Isabelle.Library hiding (quote)
+import Isabelle.Library hiding (quote, commas)
 import qualified Data.List as List
 import qualified Isabelle.Buffer as Buffer
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.XML as XML
 import qualified Isabelle.YXML as YXML