lib/Tools/expandshort
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788 df671fa2562a
parent 7887 eedfff88ee40
child 10511 efb3428c9879
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: expand shorthand goal commands
     8 
     9 
    10 PRG=$(basename "$0")
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [FILES|DIRS...]"
    16   echo
    17   echo "  Recursively find .ML files, expand shorthand goal commands.  Also"
    18   echo "  contracts uses of resolve_tac, dresolve_tac, eresolve_tac,"
    19   echo "  forward_tac, rewrite_goals_tac on 1-element lists; furthermore"
    20   echo "  expands tabs, which are forbidden in SML string constants."
    21   echo
    22   echo "  Renames old versions of files by appending \"~~\"."
    23   echo
    24   exit 1
    25 }
    26 
    27 
    28 ## process command line
    29 
    30 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
    31 
    32 SPECS="$@"; shift "$#"
    33 
    34 
    35 ## main
    36 
    37 #set by configure
    38 AUTO_PERL=perl
    39 
    40 find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/expandshort.pl"