27 echo "(**** Original file: $FILE ****)" |
27 echo "(**** Original file: $FILE ****)" |
28 echo |
28 echo |
29 if [ "$(basename "$FILE" .sig)" != "$FILE" ] |
29 if [ "$(basename "$FILE" .sig)" != "$FILE" ] |
30 then |
30 then |
31 echo -e "$FILE (global)" >&2 |
31 echo -e "$FILE (global)" >&2 |
32 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ |
32 "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \ |
33 perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \ |
33 perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \ |
34 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' |
34 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' |
35 elif fgrep -q functor "src/$FILE" |
35 elif fgrep -q functor "src/$FILE" |
36 then |
36 then |
37 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ |
37 "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \ |
38 perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \ |
38 perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \ |
39 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' |
39 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' |
40 else |
40 else |
41 echo -e "$FILE (local)" >&2 |
41 echo -e "$FILE (local)" >&2 |
42 echo "structure Metis = struct open Metis" |
42 echo "structure Metis = struct open Metis" |
43 cat < "metis_env.ML" |
43 cat < "metis_env.ML" |
44 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ |
44 "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \ |
45 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' |
45 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' |
46 echo "end;" |
46 echo "end;" |
47 fi |
47 fi |
48 done |
48 done |
49 |
49 |