# HG changeset patch
# User wenzelm
# Date 1544711574 -3600
# Node ID bbb61a9cb99adaca2381230f8b563fd47d0dfe29
# Parent  5655af3ea5bdc48eb81700e3de1e7efc5c066c38
more Haskell operations;

diff -r 5655af3ea5bd -r bbb61a9cb99a src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Dec 13 15:21:34 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Thu Dec 13 15:32:54 2018 +0100
@@ -1397,6 +1397,34 @@
     \([], a) -> App (pair term term a)]
 \<close>
 
+generate_file "Isabelle/UUID.hs" = \<open>
+{-  Title:      Isabelle/UUID.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Universally unique identifiers.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
+-}
+
+module Isabelle.UUID (random, random_string, parse)
+where
+
+import Data.UUID (UUID)
+import qualified Data.UUID as UUID
+import Data.UUID.V4 (nextRandom)
+
+
+random :: IO UUID
+random = nextRandom
+
+random_string :: IO String
+random_string = UUID.toString <$> random
+
+parse :: String -> Maybe UUID
+parse = UUID.fromString
+\<close>
+
 generate_file "Isabelle/Byte_Message.hs" = \<open>
 {-  Title:      Isabelle/Byte_Message.hs
     Author:     Makarius
diff -r 5655af3ea5bd -r bbb61a9cb99a src/Tools/Haskell/Test.thy
--- a/src/Tools/Haskell/Test.thy	Thu Dec 13 15:21:34 2018 +0100
+++ b/src/Tools/Haskell/Test.thy	Thu Dec 13 15:32:54 2018 +0100
@@ -18,7 +18,7 @@
       val _ =
         GHC.new_project tmp_dir
           {name = "isabelle",
-           depends = ["bytestring", "network", "split", "utf8-string"],
+           depends = ["bytestring", "network", "split", "utf8-string", "uuid"],
            modules = modules};
 
       val (out, rc) =