| author | paulson |
| Mon, 30 Nov 2020 19:33:07 +0000 | |
| changeset 72796 | d39a32cff5d7 |
| parent 59179 | cad8a0012a12 |
| child 78650 | 47d0c333d155 |
| permissions | -rw-r--r-- |
|
39447
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
1 |
(* Title: Tools/Metis/PortableIsabelle.sml |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
3 |
Copyright 2010 |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
4 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
5 |
Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml". |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
6 |
*) |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
7 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
8 |
structure Portable :> Portable = |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
9 |
struct |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
10 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
11 |
val ml = "isabelle" |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
12 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
13 |
fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y) |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
14 |
|
| 59179 | 15 |
local |
16 |
val lock = Mutex.mutex (); |
|
17 |
in |
|
18 |
fun critical e () = Multithreading.synchronized "metis" lock e |
|
19 |
end; |
|
|
39447
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
20 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
21 |
val randomWord = Random.nextWord |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
22 |
val randomBool = Random.nextBool |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
23 |
val randomInt = Random.nextInt |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
24 |
val randomReal = Random.nextReal |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
25 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
26 |
fun time f x = f x (* dummy *) |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
27 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
28 |
end |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
29 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
30 |
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a |