# HG changeset patch
# User blanchet
# Date 1284616458 -7200
# Node ID 61033a8004e2f3493101e76674e900d55d4cdf54
# Parent  7ed24d2dc7de33d441b37e0c4af349a1b44abb1f
put Isabelle-specifics in a "PortableIsabelle" file maintained by us;
as recommended by Joe Hurd

diff -r 7ed24d2dc7de -r 61033a8004e2 src/Tools/Metis/PortableIsabelle.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/PortableIsabelle.sml	Thu Sep 16 07:54:18 2010 +0200
@@ -0,0 +1,26 @@
+(*  Title:      Tools/Metis/PortableIsabelle.sml
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2010
+
+Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml".
+*)
+
+structure Portable :> Portable =
+struct
+
+val ml = "isabelle"
+
+fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
+
+fun critical e () = NAMED_CRITICAL "metis" e
+
+val randomWord = Random.nextWord
+val randomBool = Random.nextBool
+val randomInt = Random.nextInt
+val randomReal = Random.nextReal
+
+fun time f x = f x (* dummy *)
+
+end
+
+datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a