# HG changeset patch
# User blanchet
# Date 1284558561 -7200
# Node ID 7e8f49d412d672e96ce59fce1a8bbcf79da25ccc
# Parent  ec989bd98fc836a73705947f94c7ed1bde6ede39
rename

diff -r ec989bd98fc8 -r 7e8f49d412d6 src/Tools/Metis/make-metis
--- a/src/Tools/Metis/make-metis	Wed Sep 15 15:48:52 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-#!/usr/bin/env bash
-#
-# 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
-(*
-   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 *)
-(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
-(******************************************************************)
-
-print_depth 0;
-
-EOF
-
-  for FILE in $(cat "$THIS/FILES")
-  do
-    echo
-    echo "(**** Original file: $FILE ****)"
-    echo
-    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
-
-  cat <<EOF
-;
-print_depth 10;
-EOF
-
-) > metis.ML
diff -r ec989bd98fc8 -r 7e8f49d412d6 src/Tools/Metis/make_metis
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/make_metis	Wed Sep 15 15:49:21 2010 +0200
@@ -0,0 +1,61 @@
+#!/usr/bin/env bash
+#
+# 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
+(*
+   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 *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(******************************************************************)
+
+print_depth 0;
+
+EOF
+
+  for FILE in $(cat "$THIS/FILES")
+  do
+    echo
+    echo "(**** Original file: $FILE ****)"
+    echo
+    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
+
+  cat <<EOF
+;
+print_depth 10;
+EOF
+
+) > metis.ML