# HG changeset patch
# User wenzelm
# Date 1544620796 -3600
# Node ID dcea1fffbfe6e3597522364f14f9c096cfa02e37
# Parent  704915cf59fa6acb3647729d328c5c09abe3242d
more Haskell operations;

diff -r 704915cf59fa -r dcea1fffbfe6 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Dec 12 12:31:05 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Wed Dec 12 14:19:56 2018 +0100
@@ -25,10 +25,13 @@
 
   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 -}
@@ -91,6 +94,23 @@
 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
@@ -1112,7 +1132,7 @@
   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
diff -r 704915cf59fa -r dcea1fffbfe6 src/Tools/Haskell/Test.thy
--- a/src/Tools/Haskell/Test.thy	Wed Dec 12 12:31:05 2018 +0100
+++ b/src/Tools/Haskell/Test.thy	Wed Dec 12 14:19:56 2018 +0100
@@ -17,7 +17,9 @@
         |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
       val _ =
         GHC.new_project tmp_dir
-          {name = "isabelle", depends = ["bytestring", "utf8-string", "network"], modules = modules};
+          {name = "isabelle",
+           depends = ["bytestring", "network", "split", "utf8-string"],
+           modules = modules};
 
       val (out, rc) =
         Isabelle_System.bash_output