src/Tools/Metis/PortableIsabelle.sml
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 39447 61033a8004e2
child 59179 cad8a0012a12
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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