# HG changeset patch
# User blanchet
# Date 1284558532 -7200
# Node ID ec989bd98fc836a73705947f94c7ed1bde6ede39
# Parent  a055cffcf6fcd71904529cc82ef5562de82c1c02
use "Metis_" prefix rather than "Metis" structure;
the prefix can then be used not only for structures but also signatures and functors. A few other changes were made to the script, to eliminate the need for "metis_env.ML".

diff -r a055cffcf6fc -r ec989bd98fc8 src/Tools/Metis/make-metis
--- a/src/Tools/Metis/make-metis	Wed Sep 15 15:44:44 2010 +0200
+++ b/src/Tools/Metis/make-metis	Wed Sep 15 15:48:52 2010 +0200
@@ -10,6 +10,16 @@
 
 (
   cat <<EOF
+(*
+   This file was generated by the "make-metis" script. The BSD License is used
+   with Joe Hurd's kind permission. Extract from a September 13, 2010 email
+   written by Joe Hurd:
+
+       I hereby give permission to the Isabelle team to release Metis as part
+       of Isabelle, with the Metis code covered under the Isabelle BSD
+       license.
+*)
+
 (******************************************************************)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
@@ -18,35 +28,34 @@
 
 print_depth 0;
 
-structure Metis = struct structure Word = Word structure Array = Array end;
 EOF
 
-  for FILE in $(cat "$THIS/src/FILES")
+  for FILE in $(cat "$THIS/FILES")
   do
     echo
     echo "(**** Original file: $FILE ****)"
     echo
-    if [ "$(basename "$FILE" .sig)" != "$FILE" ]
-    then
-      echo -e "$FILE (global)" >&2
-      "$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 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 polyml "src/$FILE" | \
-      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
-      echo "end;"
-    fi
+    echo -e "$FILE" >&2
+    "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \
+    perl -p -e \
+'s/type name$/type name = string/;'\
+'s/\bref\b/Unsynchronized.ref/g;'\
+'s/\bPolyML.pointerEq\b/pointer_eq/g;'\
+'s/(?<!\.)\bexplode\b/String.explode/g;'\
+'s/(?<!\.)\bimplode\b/String.implode/g;'\
+'s/(?<!\.)\bprint\b/TextIO.print/g;'\
+'s/\bRL\b/Metis_RL/g;'\
+"`grep "^\(signature\|structure\|functor\)" src/*.{sig,sml} | \
+  sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \
+  tr " " "\n" | \
+  sort | \
+  uniq | \
+  sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`"
   done
 
-  echo "print_depth 10;"
+  cat <<EOF
+;
+print_depth 10;
+EOF
 
 ) > metis.ML