# HG changeset patch
# User wenzelm
# Date 1627677548 -7200
# Node ID 73487ebd73320622d225232ac2cd17e49d47a210
# Parent  e5e95395258d442f3a188e38f1a98852709701ab
clarified signature;

diff -r e5e95395258d -r 73487ebd7332 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Jul 30 16:21:31 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Jul 30 22:39:08 2021 +0200
@@ -193,6 +193,8 @@
 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>, \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
 -}
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
@@ -204,7 +206,7 @@
   space_explode, split_lines, trim_line, clean_name)
 where
 
-import qualified Data.List as List
+import Data.String (IsString)
 import qualified Data.List.Split as Split
 import qualified Isabelle.Symbol as Symbol
 
@@ -263,23 +265,27 @@
         Nothing -> get_aux (i + 1) xs
         Just y -> Just (i, y)
 
+separate :: a -> [a] -> [a]
+separate s (x : (xs @ (_ : _))) = x : s : separate s xs
+separate _ xs = xs;
+
 
 {- strings -}
 
-proper_string :: String -> Maybe String
-proper_string s = if null s then Nothing else Just s
-
-quote :: String -> String
+proper_string :: (IsString a, Eq a) => a -> Maybe a
+proper_string s = if s == "" then Nothing else Just s
+
+quote :: (IsString a, Semigroup a) => a -> a
 quote s = "\"" <> s <> "\""
 
-space_implode :: String -> [String] -> String
-space_implode = List.intercalate
-
-commas, commas_quote :: [String] -> String
+space_implode :: (IsString a, Monoid a) => a -> [a] -> a
+space_implode s = mconcat . separate s
+
+commas, commas_quote :: (IsString a, Monoid a) => [a] -> a
 commas = space_implode ", "
 commas_quote = commas . map quote
 
-cat_lines :: [String] -> String
+cat_lines :: (IsString a, Monoid a) => [a] -> a
 cat_lines = space_implode "\n"