# HG changeset patch
# User blanchet
# Date 1284405553 -7200
# Node ID a47de56ae6c2d6b6af8111f3bd2c3a929454f4ac
# Parent  2d0a4361c3ef31bb167684a8672f691586770d2c
update scripts

diff -r 2d0a4361c3ef -r a47de56ae6c2 src/Tools/Metis/make-metis
--- a/src/Tools/Metis/make-metis	Mon Sep 13 21:11:59 2010 +0200
+++ b/src/Tools/Metis/make-metis	Mon Sep 13 21:19:13 2010 +0200
@@ -29,19 +29,19 @@
     if [ "$(basename "$FILE" .sig)" != "$FILE" ]
     then
       echo -e "$FILE (global)" >&2
-      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+      "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \
       perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
       perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
     elif fgrep -q functor "src/$FILE"
     then
-      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+      "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \
       perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
       perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
     else
       echo -e "$FILE (local)" >&2
       echo "structure Metis = struct open Metis"
       cat < "metis_env.ML"
-      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+      "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \
       perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
       echo "end;"
     fi
diff -r 2d0a4361c3ef -r a47de56ae6c2 src/Tools/Metis/scripts/mlpp
--- a/src/Tools/Metis/scripts/mlpp	Mon Sep 13 21:11:59 2010 +0200
+++ b/src/Tools/Metis/scripts/mlpp	Mon Sep 13 21:19:13 2010 +0200
@@ -18,8 +18,8 @@
 }
 
 if (!$opt_c) { die "mlpp: you must specify the SML compiler\n"; }
-if ($opt_c ne "mosml" && $opt_c ne "mlton" && $opt_c ne "isabelle") {
-    die "mlpp: the SML compiler must be one of {mosml,mlton,isabelle}.\n";
+if ($opt_c ne "mosml" && $opt_c ne "mlton" && $opt_c ne "polyml") {
+    die "mlpp: the SML compiler must be one of {mosml,mlton,polyml}.\n";
 }
 
 # Autoflush STDIN
@@ -72,8 +72,17 @@
     my $text = shift @_;
 
     if ($opt_c eq "mosml") {
+        $text =~ s/Array\.copy/Array_copy/g;
+        $text =~ s/Array\.foldli/Array_foldli/g;
+        $text =~ s/Array\.foldri/Array_foldri/g;
+        $text =~ s/Array\.modifyi/Array_modifyi/g;
+        $text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g;
         $text =~ s/PP\.ppstream/ppstream/g;
+        $text =~ s/String\.isSuffix/String_isSuffix/g;
+        $text =~ s/Substring\.full/Substring_full/g;
         $text =~ s/TextIO\.inputLine/TextIO_inputLine/g;
+        $text =~ s/Vector\.foldli/Vector_foldli/g;
+        $text =~ s/Vector\.mapi/Vector_mapi/g;
     }
 
     print STDOUT $text;
@@ -88,7 +97,8 @@
         print STDOUT "(*#line 0.0 \"$filename\"*)\n";
     }
 
-    open my $INPUT, "$filename";
+    open my $INPUT, "$filename" or
+        die "mlpp: couldn't open $filename: $!\n";
 
     my $state = "normal";
     my $comment = 0;
@@ -173,7 +183,7 @@
                     my $pat = $2;
                     $line = $3;
                     print_normal $leadup;
-                    
+
                     if ($pat eq "`") {
                         $state = "quote";
                     }
@@ -197,7 +207,7 @@
                     }
                     elsif ($pat eq "*)") {
                         if ($revealed_comment == 0) {
-                            die "Too many comment closers.\n"
+                            die "mlpp: too many comment closers.\n"
                         }
                         --$revealed_comment;
                     }
@@ -223,13 +233,13 @@
     }
 
     if ($state eq "quote") {
-        die "EOF inside \` quote\n";
+        die "mlpp: EOF inside \` quote\n";
     }
     elsif ($state eq "dquote") {
-        die "EOF inside \" quote\n";
+        die "mlpp: EOF inside \" quote\n";
     }
     elsif ($state eq "comment") {
-        die "EOF inside comment\n";
+        die "mlpp: EOF inside comment\n";
     }
     else {
         ($state eq "normal") or die;