# HG changeset patch
# User wenzelm
# Date 1630094202 -7200
# Node ID 24a2a6ced0abb13c6af9966f6281d0af3804240b
# Parent  1a8d8dd77513589d8bb3676c4eba12a83101f7b1
more Isabelle/Haskell;

diff -r 1a8d8dd77513 -r 24a2a6ced0ab src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Aug 27 15:21:57 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Aug 27 21:56:42 2021 +0200
@@ -3242,11 +3242,12 @@
 
 module Isabelle.Time (
   Time, seconds, minutes, ms, zero, is_zero, is_relevant,
-  get_seconds, get_minutes, get_ms, message
+  get_seconds, get_minutes, get_ms, message, now
 )
 where
 
 import Text.Printf (printf)
+import Data.Time.Clock.POSIX (getPOSIXTime)
 import Isabelle.Bytes (Bytes)
 import Isabelle.Library
 
@@ -3288,6 +3289,11 @@
 
 message :: Time -> Bytes
 message t = make_bytes (show t) <> "s"
+
+now :: IO Time
+now = do
+  t <- getPOSIXTime
+  return $ Time (round (realToFrac t * 1000.0 :: Double))
 \<close>
 
 generate_file "Isabelle/Timing.hs" = \<open>