# HG changeset patch
# User blanchet
# Date 1284560193 -7200
# Node ID d4c02086dad25700432f100cc9e88512966bb1b0
# Parent  c70a6c169a161001cf61eee588e417f9d27164a5
more Isabelle-specific changes

diff -r c70a6c169a16 -r d4c02086dad2 src/Tools/Metis/src/PortablePolyml.sml
--- a/src/Tools/Metis/src/PortablePolyml.sml	Wed Sep 15 15:49:43 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml	Wed Sep 15 16:16:33 2010 +0200
@@ -44,7 +44,7 @@
             val {usr,sys} = Timer.checkCPUTimer c
             val real = Timer.checkRealTimer r
           in
-            print
+            TextIO.print (* MODIFIED by Jasmin Blanchette *)
               ("User: " ^ p usr ^ "  System: " ^ p sys ^
                "  Real: " ^ p real ^ "\n")
           end
diff -r c70a6c169a16 -r d4c02086dad2 src/Tools/Metis/src/Stream.sml
--- a/src/Tools/Metis/src/Stream.sml	Wed Sep 15 15:49:43 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sml	Wed Sep 15 16:16:33 2010 +0200
@@ -6,6 +6,8 @@
 structure Stream :> Stream =
 struct
 
+open Useful; (* MODIFIED by Jasmin Blanchette *)
+
 val K = Useful.K;
 
 val pair = Useful.pair;
diff -r c70a6c169a16 -r d4c02086dad2 src/Tools/Metis/src/Useful.sig
--- a/src/Tools/Metis/src/Useful.sig	Wed Sep 15 15:49:43 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sig	Wed Sep 15 16:16:33 2010 +0200
@@ -22,6 +22,8 @@
 (* Tracing.                                                                  *)
 (* ------------------------------------------------------------------------- *)
 
+val print : string -> unit (* MODIFIED by Jasmin Blanchette *)
+
 val tracePrint : (string -> unit) ref
 
 val trace : string -> unit
@@ -215,6 +217,10 @@
 (* Strings.                                                                  *)
 (* ------------------------------------------------------------------------- *)
 
+val implode : char list -> string (* MODIFIED by Jasmin Blanchette *)
+
+val explode : string -> char list (* MODIFIED by Jasmin Blanchette *)
+
 val rot : int -> char -> char
 
 val charToInt : char -> int option
diff -r c70a6c169a16 -r d4c02086dad2 src/Tools/Metis/src/Useful.sml
--- a/src/Tools/Metis/src/Useful.sml	Wed Sep 15 15:49:43 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml	Wed Sep 15 16:16:33 2010 +0200
@@ -50,6 +50,8 @@
 (* Tracing.                                                                  *)
 (* ------------------------------------------------------------------------- *)
 
+val print = TextIO.print; (* MODIFIED by Jasmin Blanchette *)
+
 val tracePrint = ref print;
 
 fun trace mesg = !tracePrint mesg;
@@ -496,6 +498,10 @@
 (* Strings.                                                                  *)
 (* ------------------------------------------------------------------------- *)
 
+val implode = String.implode (* MODIFIED by Jasmin Blanchette *)
+
+val explode = String.explode (* MODIFIED by Jasmin Blanchette *)
+
 local
   fun len l = (length l, l)