--- 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