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