equal
deleted
inserted
replaced
1 #! /bin/sh |
1 #! /bin/sh |
2 # $Id$ |
2 # $Id$ |
3 #Shell script to expand shorthand goal commands |
3 #Shell script to expand shorthand goal commands |
4 # ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
4 # ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
5 # rewrite_goals_tac on 1-element lists |
5 # rewrite_goals_tac on 1-element lists |
|
6 # ALSO expands tabs, since they are now forbidden in strings. |
6 # |
7 # |
7 # Usage: |
8 # Usage: |
8 # expandshort FILE1 ... FILEn |
9 # expandshort FILE1 ... FILEn |
9 # |
10 # |
10 #Renames old versions of the files as FILE1~~ ... FILEn~~ |
11 #Renames old versions of the files as FILE1~~ ... FILEn~~ |
24 s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/ |
25 s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/ |
25 s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g |
26 s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g |
26 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g |
27 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g |
27 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g |
28 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g |
28 s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g |
29 s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g |
29 ' $f~~ > $f |
30 ' $f~~ | expand > $f |
30 done |
31 done |
31 echo Finished. |
32 echo Finished. |