equal
deleted
inserted
replaced
9 # global! |
9 # global! |
10 |
10 |
11 THIS=$(cd "$(dirname "$0")"; echo $PWD) |
11 THIS=$(cd "$(dirname "$0")"; echo $PWD) |
12 |
12 |
13 ( |
13 ( |
|
14 echo -n '(* $' |
|
15 echo 'Id$ *)' |
14 cat <<EOF |
16 cat <<EOF |
15 (******************************************************************) |
17 (******************************************************************) |
16 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
18 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
17 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
19 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
18 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
20 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
38 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ |
40 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ |
39 perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' |
41 perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' |
40 else |
42 else |
41 echo -e "$FILE (local)" >&2 |
43 echo -e "$FILE (local)" >&2 |
42 echo "structure Metis = struct open Metis" |
44 echo "structure Metis = struct open Metis" |
43 cat < "metis-env.ML" |
45 cat < "metis_env.ML" |
44 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" |
46 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" |
45 echo "end;" |
47 echo "end;" |
46 fi |
48 fi |
47 done |
49 done |
48 |
50 |