| author | blanchet |
| Thu, 16 Sep 2010 07:54:18 +0200 | |
| changeset 39447 | 61033a8004e2 |
| child 59179 | cad8a0012a12 |
| 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 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
15 |
fun critical e () = NAMED_CRITICAL "metis" e |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
16 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
17 |
val randomWord = Random.nextWord |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
18 |
val randomBool = Random.nextBool |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
19 |
val randomInt = Random.nextInt |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
20 |
val randomReal = Random.nextReal |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
21 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
22 |
fun time f x = f x (* dummy *) |
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
23 |
|
|
61033a8004e2
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
blanchet
parents:
diff
changeset
|
24 |
end |
|
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 |
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a |