src/Tools/expandshort
changeset 1445 887e9816eea4
parent 819 8928f1c44d80
child 1567 02bbdc811ae7
equal deleted inserted replaced
1444:23ceb1dc9755 1445:887e9816eea4
     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.