| author | wenzelm |
| Wed, 01 Mar 2023 13:30:35 +0100 | |
| changeset 77438 | 0030eabbe6c3 |
| parent 73383 | 6b104dc069de |
| child 82092 | 93195437fdee |
| permissions | -rw-r--r-- |
|
73383
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/General/time.scala |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
3 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
4 |
Time based on nanoseconds (idealized). |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
6 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
7 |
signature TIME = |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
8 |
sig |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
9 |
include TIME |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
10 |
val min: time * time -> time |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
11 |
val max: time * time -> time |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
12 |
val scale: real -> time -> time |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
13 |
end; |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
14 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
15 |
structure Time: TIME = |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
16 |
struct |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
17 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
18 |
open Time; |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
19 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
20 |
fun min (t1, t2) = if t1 < t2 then t1 else t2; |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
21 |
fun max (t1, t2) = if t1 > t2 then t1 else t2; |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
22 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
23 |
fun scale s t = Time.fromNanoseconds (Real.ceil (s * Real.fromInt (Time.toNanoseconds t))); |
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
24 |
|
|
6b104dc069de
clarified signature --- augment existing structure Time;
wenzelm
parents:
diff
changeset
|
25 |
end; |