--- 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>