lib/Tools/fixdots
author wenzelm
Fri Oct 10 14:51:58 1997 +0200 (1997-10-10)
changeset 3826 0caedb36900d
parent 3825 478461d77e88
child 4508 f102cb0140fe
permissions -rwxr-xr-x
tuned;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: ensure that dots in formulas are followed by non-idents
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG=$(basename $0)
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [FILES|DIRS...]"
    16   echo
    17   echo "  Recursively find .thy/.ML files, patching them to ensure that"
    18   echo "  dots in formulas are followed by non-idents."
    19   echo
    20   echo "  Renames old versions of FILES by appending \"~~\"."
    21   echo
    22   exit 1
    23 }
    24 
    25 
    26 ## process command line
    27 
    28 [ $# -eq 0 -o "$1" = "-?" ] && usage
    29 
    30 SPECS="$@"; shift $#
    31 
    32 
    33 ## main
    34 
    35 PERL=$(type -path perl)
    36 if [ -z $PERL ]; then
    37   echo "$PRG fatal error: no perl!?"
    38 else
    39   find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    40     xargs $PERL $ISABELLE_HOME/lib/scripts/fixdots.pl
    41 fi