diff -r ee218296d635 -r 028e39e5e8f3 src/Tools/Metis/make-metis
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/make-metis	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+#
+# $Id$
+#
+# make-metis - turn original Metis files into Isabelle ML source.
+#
+# Structure declarations etc. are made local by wrapping into a
+# collective structure Metis.  Signature and functor definitions are
+# global!
+
+THIS=$(cd "$(dirname "$0")"; echo $PWD)
+
+(
+  cat <<EOF
+(******************************************************************)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(******************************************************************)
+
+print_depth 0;
+
+structure Metis = struct end;
+EOF
+
+  for FILE in $(cat "$THIS/src/FILES")
+  do
+    echo
+    echo "(**** Original file: $FILE ****)"
+    echo
+    if [ "$(basename "$FILE" .sig)" != "$FILE" ]
+    then
+      echo -e "$FILE (global)" >&2
+      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;'
+    elif fgrep -q functor "src/$FILE"
+    then
+      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;'
+    else
+      echo -e "$FILE (local)" >&2
+      echo "structure Metis = struct open Metis"
+      cat < "metis-env"
+      "$THIS/scripts/mlpp" -c isabelle "src/$FILE"
+      echo "end;"
+    fi
+  done
+
+  echo "print_depth 10;"
+
+) > metis.ML