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